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 NuCalculus.
In Proc. of the 19th Annual Symposium in Logic in Computer Science (LICS),
pages 150159, 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
MetaLanguages: Theory and Practice (LFMTP), pages 6977, 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 SIGPLANSIGACT Symposium on Principles of
Programming Languages (POPL), pages 315, ACM, 2008.
[bib]
 J. Bengtson and J. Parrow,
Formalising the PiCalculus 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 6377, SpringerVerlag, 2007.
[bib]
 J. Bengtson and J. Parrow,
A Completeness Proof for Bisimulation in the piCalculus 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 86101, SpringerVerlag, 2005.
[bib]
 S. Berghofer and C. Urban,
A HeadtoHead Comparison of de Bruijn Indices and Names.
In Proc. of the International Workshop on Logical Frameworks and
MetaLanguages: Theory and Practice (LFMTP 2006). Electronic Notes in Theoretical
Computer Science. Vol. 174(5). Pages 5367.
 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 332334, SpringerVerlag, 2004.
[bib]
 J. Cheney,
Nominal Logic Programming.
PhDThesis, Cornell University, 2004.
[bib]
 J. Cheney,
Relating HigherOrder Pattern Unification and Nominal Unification.
In Proc. of UNIF 2005, p. 104119.
 J. Cheney,
Completeness and Herbrand Theorems for Nominal Logic.
Journal of Symbolic Logic 71(1), 299320, 2006.
[bib]
 J. Cheney,
The Semantics of Nominal Logic Programs.
In Proc. of ICLP 2006, p. 361375.
 J. Cheney,
Scrap your Nameplate (Functional Pearl).
In Proc. of the 10th International Conference on Functional Programming (ICFP),
pages 180191, 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 2532, 2005.
[bib]
 J. Cheney,
Simple Nominal Type Theory.
Draft, 2008.
 J. Cheney and A. Momigliano,
Mechanized Metatheory ModelChecking.
In Proc. of the 9th ACM SIGPLAN Symposium on Principles
and Practice of Declarative Programming (PPDP), pages 7586, 2007.
 J. Cheney and C. Urban,
AlphaProlog: A Logic Programming Language with Names, Binding and AlphaEquivalence.
 J. Cheney and C. Urban,
System Description: AlphaProlog, a Fresh Approach to Logic Programming
Modulo AlphaEquivalence.
 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 108119, 2004.
 M. J. Gabbay,
The PiCalculus in FraenkelMostowski.
 M. J. Gabbay,
Automating FraenkelMostowski Syntax.
 M. J. Gabbay,
FMHOL, a HigherOrder Theory of Names.
 M. J. Gabbay,
A Theory of Inductive Definitions with AlphaEquivalence.
PhDThesis, 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:341363, 2002.
An earlier version of this paper appeared in the Proc. of the 14th Symposium on
Logic in Computer Science (LICS), pages 214224, 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.
PhDThesis, 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 4149, 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 MetaLanguages:
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 241256, Springer Verlag, 2004.
[bib]
 M. Norrish,
Mechanising LambdaCalculus using a Classical First Order Theory of
Terms with Permutations.
Higher Order and Symbolic Computation, 19:169195, 2006.
[bib]
 M. Norrish and R. Vestergaard,
Proof Pearl: de Bruijn Terms Really do Work.
TPHOLs 2007.
 A. M. Pitts,
AlphaStructural Recursion and Induction.
Journal of the ACM 53(2006)459506.
[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 1734, Springer Verlag, 2005.
[bib]
 A. M. Pitts,
Nominal Logic, A First Order Theory of Names and Binding.
Information and Computation 186(2003) 165193. 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 219242, 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 230255, Springer Verlag, 2000.
[bib]
 A. M. Pitts and M. R. Shinwell,
Generative Unbinding of Names.
In Proc. of the 34th Annual ACM SIGPLANSIGACT Symposium on Principles of
Programming Languages (POPL), pages 8595, 2007.
 F. Pottier,
Static Name Control for FreshML.
In Proc. of the 22nd Annual IEEE Symposium on Logic In Computer Science (LICS), pages 356365, 2007.
 U. Schöpp,
Names and Binding in Type Theory.
PhDThesis, 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 235249, SpringerVerlag, 2004.
[bib]
 U. Schöpp,
Modelling Generic Judgements.
In Proc. of the International Workshop on Logical Frameworks and
MetaLanguages: 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.
PhDThesis, Cambridge University, 2005.
[bib]
 M. R. Shinwell and A. M. Pitts,
Fresh Objective Caml User Manual.
University of Cambridge Computer Laboratory Technical Report UCAMCLTR621, 2005.
[bib]
 M. R. Shinwell and A. M. Pitts,
On a Monadic Semantics for Freshness.
Theoretical Computer Science 342 (2005) 2855.
[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 263274, ACM Press, 2003.
[bib]
 S. Staton,
NamePassing Process Calculi: Operational Models and Structural Operational Semantics.
PhDThesis, 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 lamdatree syntax specifications.
In Proc. of the International Workshop on Logical Frameworks and MetaLanguages:
Theory and Practice (LFMTP), 2008.
 C. Urban,
Nominal Techniques in Isabelle/HOL.
In Journal of Automated Reasoning, Volume 40(4), pages 327356, 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 498512, SpringerVerlag 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 3550,
SpringerVerlag, 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 2523, 2005. [bib]
 C. Urban and J. Cheney,
Avoiding Equivariance in AlphaProlog.
In Proc. of the 7th International Conference on Typed Lambda
Calculi and Applications (TLCA), Lecture Notes in Computer
Science, Volume 3461, pages 401416, SpringerVerlag, 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 4556, 2008.
 C. Urban, A. M. Pitts and M. J. Gabbay,
Nominal Unification. Theoretical Computer Science 323 (2004), pages 473497.
[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 513527, SpringerVerlag, 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 3853, SpringerVerlag, 2005.
[bib]
 C. Urban and B. Zhu,
Revisiting CutElimination: 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 409424, 2008.
 J. A. Vaughan,
Review of Three Techniques for Formally Representing Variable Binding.
Technical Report MSCIS0619, 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 123134, 2008.
