Tags

# Group: Nominal techniques - library 119 articles

## General Bindings and Alpha-Equivalence in Nominal Isabelle

[CiTO]
Logical Methods in Computer Science, Vol. 8, No. 2:14. (2012)
posted to no-tag by cu to the group Nominal techniques on 2012-07-08 06:36:31

## Nominal Logic with Equations Only

[CiTO]
In Proceedings of the Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2011), Vol. 71 (2011), pp. 44-57
posted to no-tag by Ranald_Clouston to the group Nominal techniques on 2011-11-18 02:53:49

## Nominal Lawvere Theories

[CiTO]
In Logic, Language, Information and Computation: 18th International Workshop, WoLLIC 2011, Philadelphia, PA, USA, May 18-20, Proceedings, Vol. 6642 (2011), pp. 67-83, doi:10.1007/978-3-642-20920-8_11
posted to no-tag by Ranald_Clouston to the group Nominal techniques on 2011-09-23 00:40:40

## Constraint Solving in Non-Permutative Nominal Abstract Syntax

[CiTO]
Logical Methods in Computer Science, Vol. 7, No. 3:6. (August 2011)
posted to no-tag by andrewmpitts to the group Nominal techniques on 2011-09-14 07:17:30

## General Bindings and Alpha-Equivalence in Nominal Isabelle

[CiTO]
In Proceedings of the 20th European Symposium on Programming (ESOP), Vol. 6602 (2011), pp. 480-500
posted to no-tag by cu to the group Nominal techniques on 2011-04-21 16:45:55

## Psi-Calculi: Mobile Processes, Nominal Data, and Logic

[CiTO]
In Twenty-Fourth Annual {IEEE} Symposium on Logic in Computer Science ({LICS} 2009), Los Angeles, USA (August 2009), pp. 39-48
posted to no-tag by andrewmpitts to the group Nominal techniques on 2010-10-16 08:46:15

## Binding in Nominal Equational Logic

[CiTO]
Electronic Notes in Theoretical Computer Science, Vol. 265, No. C. (2010), pp. 259-276
posted to no-tag by andrewmpitts to the group Nominal techniques on 2010-09-24 09:34:30 along with 1 person

## Proof Pearl: A New Foundation for Nominal Isabelle

[CiTO]
In Proceecings of the 1st Conference on Interactive Theorem Proving, Vol. 6172 (2010), pp. 35-50
posted to no-tag by cu to the group Nominal techniques on 2010-07-21 10:57:07

### Abstract

Pitts et al introduced a beautiful theory about names and binding based on the notions of permutation and support. The engineering challenge is to smoothly adapt this theory to a theorem prover environment, in our case Isabelle/HOL.We present a formalisation of this work that differs from our earlier approachin two important respects: First, instead of representing permutations aslists of pairs of atoms, we now use a more abstract representation based onfunctions. Second, whereas the earlier work modeled different sorts of ...

## $\α$LeanTAP: A Declarative Theorem Prover for First-Order Classical Logic

[CiTO]
In Proceedings of the 24$^\\mathrm{th}$ International Conference on Logic Programming {(ICLP 2008)} (2008), pp. 238-252
posted to file-import-10-01-03 by dpm_edinburgh to the group Nominal techniques on 2010-01-03 16:29:01

## On Normalization by Evaluation for Object Calculi

[CiTO]
In Proceedings of the Conference of the Types Project {(TYPES 2007)}, Vol. 4941 (2008), pp. 173-187
posted to file-import-09-11-09 by dpm_edinburgh to the group Nominal techniques on 2009-11-09 10:47:26

## Nominal renaming sets

[CiTO]
In Proceedings of the International Conference on Logic for Programming, Artificial Intelligence and Reasoning {(LPAR 2008}), Vol. 5330 (2008), pp. 158-173
posted to file-import-09-11-09 by dpm_edinburgh to the group Nominal techniques on 2009-11-09 10:47:26

## A Study of Substitution using Fraenkel-Mostowski sets

[CiTO]
Theoretical Computer Science, Vol. 410 (2008), pp. 1159-1189
posted to file-import-09-11-09 by dpm_edinburgh to the group Nominal techniques on 2009-11-09 10:47:26

## Nominal (Universal) Algebra

[CiTO]
Journal of Information and Computation (2009)
posted to file-import-09-11-09 by dpm_edinburgh to the group Nominal techniques on 2009-11-09 10:47:26

to appear

## Nominal Renaming Sets

[CiTO]
No. HW-MACS-TR-0058. (2007)
posted to by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Nominal Algebra and the HSP Theorem

[CiTO]
No. HW-MACS-TR-0057. (2007)
posted to by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Nominal Algebra

[CiTO]
No. HW-MACS-TR-0045. (2006)
posted to by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10 along with 1 person

## Name-Passing Process Calculi: Operational Models and Structural Operational Semantics

[CiTO]
(2006)
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## The Fresh Approach: Functional Programming with Names and Binders

[CiTO]
(2005)
posted to by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Logical Calculi for Reasoning with Binding

[CiTO]
(2007)
posted to by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## A Theory of Inductive Definitions with $\α$-equivalence

[CiTO]
(2000)
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Nominal Logic Programming

[CiTO]
(2004)
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## How to Prove False using the Variable Convention

[CiTO]
(2008)
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## The Nominal Datatype Package (Preliminary Manual)

[CiTO]
(2007)
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Implementing Secure Broadcast Ambients in Isabelle using Nominal Logic

[CiTO]
In Emerging Trends Report of the 21$^\\mathrm{st}$ International Conference on Theorem Proving in Higher Order Logics {(TPHOLs 2008)} (2008), pp. 123-134
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof

[CiTO]
In Proceedings of the 19$^\\mathrm{th}$ International Conference on Rewriting Techniques and Applications {(RTA 2008)} (2008), pp. 409-424
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## A Recursion Operator for Nominal Datatypes Implemented in Isabelle/HOL

[CiTO]
In Proceedings of the 3$^\\mathrm{rd}$ International Joint Conference on Automated Deduction {(IJCAR 2006)} (2006), pp. 498-512
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Nominal Techniques in Isabelle/HOL

[CiTO]
In Proceedings of the 20th Conference on Automated Deduction ({CADE}), Vol. 3632 (2005), pp. 38-53
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Mechanizing the Metatheory of LF

[CiTO]
In Logic in Computer Science ({LICS} 2008) (2008), pp. 45-46
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## A Formal Treatment of the Barendregt Convention in Rule Inductions (Extended Abstract)

[CiTO]
In Proceedings of the {ACM} Workshop on Mechanized Reasoning about Languages with Variable Binding and Names ({MERLIN} 2005) (2005), pp. 25-32
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Barendregt's Variable Convention in Rule Inductions

[CiTO]
In Proceedings of the 21$^\\mathrm{st}$ International Conference on Automated Deduction {(CADE-21)} (2007), pp. 35-50
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Avoiding Equivariance in $\α$-Prolog

[CiTO]
In Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications ({TLCA 2005}) (2005), pp. 401-416
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Full Abstraction for Nominal General References

[CiTO]
In Proceedings of the 22$^\\mathrm{nd}$ Annual {IEEE} Symposium on Logic in Computer Science {(LICS 2007)} (2007), pp. 399-410
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## On the Role of Names in Reasoning about $\λ$-tree Syntax

[CiTO]
In Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice ({LFMTP 2008}) (2008)
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Swapping the Atom: Programming with Binders in FreshO'Caml

[CiTO]
In Proceedings of the 2$^\\mathrm{nd}$ {ACM SIGPLAN} Workshop on Mechanized Reasoning about Languages with Variable Binding ({MERLIN 2003}) (2003)
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## FreshML: Programming with Binders Made Simple

[CiTO]
In Eighth {ACM SIGPLAN} International Conference on Functional Programming ({ICFP} 2003), Uppsala, Sweden (2003), pp. 263-274
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## A Dependent Type Theory with Names and Binding

[CiTO]
In Computer Science Logic, Vol. 3210 (2004), pp. 235-249
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Static Name Control for FreshML

[CiTO]
In LICS '07: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science (2007), pp. 356-365
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Nominal System T

[CiTO]
In Proceedings of the 37$^\\mathrm{th}$ {ACM SIGACT-SIGPLAN} Symposium on Principles of Programming Languages {(POPL 2010)} (2010)
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

To appear

## A Metalanguage for Programming with Bound Names Modulo Renaming

[CiTO]
In Proceedings of 5th International Conference on the Mathematics of Program Construction. {(MPC2000)}, Vol. 1837 (2000), pp. 230-255
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Equivariant Syntax and Semantics

[CiTO]
In International Colloquium on Automata, Languages and Programming ({ICALP}) (2002), pp. 32-36
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Proof Pearl: de Bruijn Terms Really do Work

[CiTO]
In Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics ({TPHOLS 2007}) (2007), pp. 207-222
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Nominal Verification of Typical SOS Proofs

[CiTO]
In Proceedings of the 3$^\\mathrm{rd}$ Workshop on Logical and Semantic Frameworks with Applications {(LFSA 2008)} (2009), pp. 139-155
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Nominal SOS

[CiTO]
In Proceedings of the 18th Nordic Workshop on Programming Theory ({NWPT'06}) (2006)
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Translating Specifications from Nominal Logic to CIC with the Theory of Contexts

[CiTO]
In Proceedings of the 3$^\\mathrm{rd}$ {ACM SIGPLAN} Workshop on Mechanized Reasoning about Languages with Variable Binding {(MERLIN 2005)} (2005), pp. 41-49
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Nominal Unification from a Higher-Order Perspective

[CiTO]
In Proceedings of the 19$^\\mathrm{th}$ international conference on Rewriting Techniques and Applications {(RTA 2008)} (2008), pp. 246-260
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming

[CiTO]
In Proceedings of the 18$^\\mathrm{th}$ European Symposium on Programming {(ESOP 2009)}, Vol. 5502 (2009), pp. 47-61
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Representing Names with Variables in Nominal Abstract Syntax

[CiTO]
In Informal Proceedings of the 2$^\\mathrm{nd}$ International Workshop on Theory and Applications of Abstraction, Substitution and Naming ({TAASN 2009}) (2009)
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Towards Universal Algebra over Nominal Sets

[CiTO]
In Informal Proceedings of Topology, Algebra and Categories in Logic {(TACL 2009)} (2009)
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Implementing Spi Calculus Using Nominal Techniques

[CiTO]
In Proceedings of the 4$^\\mathrm{th}$ conference on Computability in Europe {(CiE 2008)} (2008), pp. 294-305
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10

## Universal algebra over $\λ$-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables

[CiTO]
In Informal Proceedings of the 4$^\\mathrm{th}$ International Workshop on Logical Frameworks and Meta-languages: Theory and Practice ({LFMTP 2009}) (2009)
posted to file-import-09-10-27 by dpm_edinburgh to the group Nominal techniques on 2009-10-27 16:36:10