Some Nominal Papers

S. Abramsky, D. R. Ghica, A. S. Murawski, C.-H. L. Ong and I. D. R. Stark, Nominal Games and Full Abstraction for the Nu-Calculus. In Proc. of the 19th Annual Symposium in Logic in Computer Science (LICS), pages 150-159, IEEE Computer Science Press, 2004. [bib]

B. Aydemir, A. Bohannon and S. Weirich, Nominal Reasoning Techniques in Coq (Extended Abstract). In Proc. of the 1st International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), pages 69-77, ENTCS, Elsevier, 2007. [bib]

B. Aydemir, A. Charguéraud, B. C. Pierce, R. Pollack and S. Weirich, Engineering Formal Metatheory. In Proc. of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 3-15, ACM, 2008. [bib]

J. Bengtson and J. Parrow, Formalising the Pi-Calculus using Nominal Logic. In Proc. of the 10th International Conference on Foundations of Software Science and Computation Structures (FOSSACS). Lecture Notes in Computer Science, Volume 4423, pages 63-77, Springer-Verlag, 2007. [bib]

J. Bengtson and J. Parrow, A Completeness Proof for Bisimulation in the pi-Calculus using Isabelle. In Proc. of the 4th Workshop on Structural Operational Semantics (SOS), 2007.

N. Benton and B. Leperchey, Relational Reasoning in a Nominal Semantics for Storage. In Proc. of the 7th International Conference on Typed Lambda Calculi and Applications (TLCA). Lecture Notes in Computer Science, Volume 3461, pages 86-101, Springer-Verlag, 2005. [bib]

S. Berghofer and C. Urban, A Head-to-Head Comparison of de Bruijn Indices and Names. In Proc. of the International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2006). Electronic Notes in Theoretical Computer Science. Vol. 174(5). Pages 53-67.

S. Berghofer and C. Urban, Nominal Inversion Principles. Accepted at TPHOLs, 2008.

J. Cheney, The Complexity of Equivariant Unification. In Proc. of the 31st International Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science, Volume 3142, pages 332-334, Springer-Verlag, 2004. [bib]

J. Cheney, Nominal Logic Programming. PhD-Thesis, Cornell University, 2004. [bib]

J. Cheney, Relating Higher-Order Pattern Unification and Nominal Unification. In Proc. of UNIF 2005, p. 104-119.

J. Cheney, Completeness and Herbrand Theorems for Nominal Logic. Journal of Symbolic Logic 71(1), 299-320, 2006. [bib]

J. Cheney, The Semantics of Nominal Logic Programs. In Proc. of ICLP 2006, p. 361-375.

J. Cheney, Scrap your Nameplate (Functional Pearl). In Proc. of the 10th International Conference on Functional Programming (ICFP), pages 180-191, ACM Press, 2005. [bib]

J. Cheney, Towards a General Theory of Names, Binding and Scope. In Proc. of the 3rd International ACM Workshop on Mechanized Reasoning about Languages with Variable Binding and Names (MERLIN), pages 25-32, 2005. [bib]

J. Cheney, Simple Nominal Type Theory. Draft, 2008.

J. Cheney and A. Momigliano, Mechanized Metatheory Model-Checking. In Proc. of the 9th ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP), pages 75-86, 2007.

J. Cheney and C. Urban, Alpha-Prolog: A Logic Programming Language with Names, Binding and Alpha-Equivalence.

J. Cheney and C. Urban, System Description: Alpha-Prolog, a Fresh Approach to Logic Programming Modulo Alpha-Equivalence.

J. Cheney and C. Urban, Nominal Logic Programming. Accepted for publication in Transactions on Programming Languages and Systems.

R. A. Clouston and A. M. Pitts, Nominal Equational Logic. In Festschrift for Gordon Plotkin, Electronic Notes in Theoretical Computer Science, Volume 1496, to appear.

L. Dixon and A. Smaill and A. Bundy, Planning as Deductive Synthesis in Intuitionistic Linear Logic. Informatics Technical Report 0786, Edinburgh University, 2006.

M. Fernandez, M. J. Gabbay and I. Mackie, Nominal Rewriting. In Proc. of Principles and Practice of Declarative Programming, pages 108-119, 2004.

M. J. Gabbay, The Pi-Calculus in Fraenkel-Mostowski.

M. J. Gabbay, Automating Fraenkel-Mostowski Syntax.

M. J. Gabbay, FM-HOL, a Higher-Order Theory of Names.

M. J. Gabbay, A Theory of Inductive Definitions with Alpha-Equivalence. PhD-Thesis, Cambridge University, 2001. [bib]

M. J. Gabbay, Hierarchical Nominal Rewriting.

M. J. Gabbay and J. Cheney, A Proof Theory for Nominal Logic.

M. J. Gabbay and J. Cheney, A Sequent Calculus for Nominal Logic.

M. J. Gabbay and A. M. Pitts, A New Approach to Abstract Syntax Involving Binders. In Formal Aspects of Computing 13:341-363, 2002.

An earlier version of this paper appeared in the Proc. of the 14th Symposium on Logic in Computer Science (LICS), pages 214-224, 1999.


T. Kahsai and M. Miculan, Implementing Spi Calculus using Nominal Techniques. In Proc of the 4th Conference on Computability in Europe (CiE), Lecture Notes in Computer Science, volume 5028, 2008.

M. R. Lakin and A. M. Pitts, A Metalanguage for Structural Operational Semantics. In Draft Proc. of the 8th Symposium on Trends in Functional Programming (TFP), 2007.

A. Mathijssen, Logical Calculi for Reasoning with Binding. PhD-Thesis, University of Eindhoven, 2007. [bib]

M. Miculan, I. Scagnetto and F. Honsell, Translating Specifications from Nominal Logic to CIC with the Theory of Contexts. Proc. of the 3rd ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN), pages 41-49, 2005.

J. Narboux and C. Urban, Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking. In Proceedings of the International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2007). To appear in Electronic Notes in Theoretical Computer Science.

M. Norrish, Recursive Function Definition for Types with Binders. In Proc. of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs), Lecture Notes in Computer Science, Volume 3223, pages 241-256, Springer Verlag, 2004. [bib]

M. Norrish, Mechanising Lambda-Calculus using a Classical First Order Theory of Terms with Permutations. Higher Order and Symbolic Computation, 19:169-195, 2006. [bib]

M. Norrish and R. Vestergaard, Proof Pearl: de Bruijn Terms Really do Work. TPHOLs 2007.

A. M. Pitts, Alpha-Structural Recursion and Induction. Journal of the ACM 53(2006)459-506. [bib]

An extended abstract appeard in Proc. of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs), Lecture Notes in Computer Science, Volume 3603, pages 17-34, Springer Verlag, 2005. [bib]


A. M. Pitts, Nominal Logic, A First Order Theory of Names and Binding. Information and Computation 186(2003) 165-193. Special issue on TACS2001. [bib]

A preliminary version of this paper appeared in Proc. of the 4th International Symposium on Theoretical Aspects of Computer Software (TACS), Lecture Notes in Computer Science, Volume 2215, pages 219-242, Springer Verlag, 2001.


A. M. Pitts and M. J. Gabbay, A Metalanguage for Programming with Bound Names Modulo Renaming. In Proc. of the 5th International Conference on Mathematics of Programme Construction, Lecture Notes in Computer Science, Volume 1837, pages 230-255, Springer Verlag, 2000. [bib]

A. M. Pitts and M. R. Shinwell, Generative Unbinding of Names. In Proc. of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 85-95, 2007.

F. Pottier, Static Name Control for FreshML. In Proc. of the 22nd Annual IEEE Symposium on Logic In Computer Science (LICS), pages 356-365, 2007.

U. Schöpp, Names and Binding in Type Theory. PhD-Thesis, Edinburgh University, 2006.

U. Schöpp and I. Stark, A Dependent Type Theory with Names and Binding. Proc. of the 13th Conference on Computer Science Logic (CSL), Lecture Notes in Computer Science, Volume 3210, pages 235-249, Springer-Verlag, 2004. [bib]

U. Schöpp, Modelling Generic Judgements. In Proc. of the International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2006).

M. R. Shinwell, Swapping the Atom: Programming with Binders in Fresh O'Caml. (presented at MERLIN 2003 - no bibliographic information available)

M. R. Shinwell, Fresh O'Caml: Nominal Abstract Syntax for the Masses. (appeared(?) in Electronic Notes in Theoretical Computer Science - no bibliographic information available)

M. R. Shinwell, The Fresh Approach: Functional Programming with Names and Binders. PhD-Thesis, Cambridge University, 2005. [bib]

M. R. Shinwell and A. M. Pitts, Fresh Objective Caml User Manual. University of Cambridge Computer Laboratory Technical Report UCAM-CL-TR-621, 2005. [bib]

M. R. Shinwell and A. M. Pitts, On a Monadic Semantics for Freshness. Theoretical Computer Science 342 (2005) 28-55. [bib]

A preliminary version appeared in Proc. of the 2nd Workshop of the Thematic Network APPSEM II, Tallinn, Estonia, April 2004.


M. R. Shinwell, A. M. Pitts and M. J. Gabbay, FreshML: Programming with Binders Made Simple. In Proc. of the 8th International Conference on Functional Programming (ICFP), pages 263-274, ACM Press, 2003. [bib]

S. Staton, Name-Passing Process Calculi: Operational Models and Structural Operational Semantics. PhD-Thesis, Cambridge University, 2006.

N. Tzevelekos, Full Abstraction for Nominal General References. In Proc. of the 22nd Annual IEEE Symposium on Logic In Computer Science (LICS), pages ??, 2007.

A. Tiu, On the role of names in reasoning about lamda-tree syntax specifications. In Proc. of the International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2008.

C. Urban, Nominal Techniques in Isabelle/HOL. In Journal of Automated Reasoning, Volume 40(4), pages 327-356, 2008. [bib]

C. Urban and S. Berghofer, A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. In Proc. of the 3rd International Joint Conference on Automated Deduction (IJCAR), Lecture Notes in Artificial Intelligence, Volume 4130, pages 498-512, Springer-Verlag 2006. [bib]

C. Urban, S. Berghofer and M. Norrish, Barendregt's Variable Convention in Rule Inductions. In Proc. of the 21th International Conference on Automated Deduction (CADE), Lecture Notes in Artificial Intelligence, Volume 4603, pages 35-50, Springer-Verlag, 2007. [bib]

A preliminary version of this paper appeared as A Formal Treatment of the Barendregt Variable Convention in Rule Inductions. In Proc. of the 3rd International ACM Workshop on Mechanized Reasoning about Languages with Variable Binding and Names (MERLIN), pages 25-23, 2005. [bib]


C. Urban and J. Cheney, Avoiding Equivariance in Alpha-Prolog. In Proc. of the 7th International Conference on Typed Lambda Calculi and Applications (TLCA), Lecture Notes in Computer Science, Volume 3461, pages 401-416, Springer-Verlag, 2005. [bib]

C. Urban, J. Cheney and S. Berghofer, Mechanising the Metatheory of LF. In Proc. of the 23rd IEEE Symposium on Logic in Computer Science (LICS 2008), IEEE Computer Society, pages 45-56, 2008.

C. Urban, A. M. Pitts and M. J. Gabbay, Nominal Unification. Theoretical Computer Science 323 (2004), pages 473-497. [bib]

A preliminary version apeared in Proc. of the 12th Conference on Computer Science Logic and 8th Kurt Godel Colloquium (CSL & KGC), Lecture Notes in Computer Science, Volume 2803, pages 513-527, Springer-Verlag, 2003.


C. Urban and C. Tasson, Nominal Reasoning Techniques in Isabelle/HOL. In Proc. of the 20th International Conference on Automated Deduction (CADE), Lecture Notes in Computer Science, Volume 3632, pages 38-53, Springer-Verlag, 2005. [bib]

C. Urban and B. Zhu, Revisiting Cut-Elimination: One Difficult Proof is Really a Proof. In Proc. of the 19th International Conference on Rewriting Techniques and Applications (RTA). In Volume 5117 of Lecture Notes in Computer Science, pages 409-424, 2008.

J. A. Vaughan, Review of Three Techniques for Formally Representing Variable Binding. Technical Report MS-CIS-06-19, University of Pennsylvania, 2006.

A. Yasmeen and E. Gunter, Implementing Secure Broadcast Ambients in Isabelle using Nominal Logic. In the Ermerging Trends Report of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs'08), Concordia University, pages 123-134, 2008.

Last modified: Sat Aug 23 17:40:43 CEST 2008 [Validate this page.]