Andrea Asperti, Claudo Sacerdoti Coen, Enrico Tassi & Stefano Zacchiroli (2007):
Crafting a Proof Assistant,
pp. 18–32,
Lecture Notes in Computer Science.
Springer,
doi:10.1007/978-3-540-74464-1_2.
Christoph Benzmüller, Chad E. Brown & Michael Kohlhase (2004):
Higher-order semantics and extensionality.
Journal of Symbolic Logic 69,
pp. 1027–1088,
doi:10.2178/jsl/1102022211.
James Cheney & Christian Urban (2004):
Alpha-Prolog: A Logic Programming Language with Names, Binding and Alpha-Equivalence.
In: Bart Demoen & Vladimir Lifschitz: Proceedings of the 20th International Conference on Logic Programming (ICLP 2004),
Lecture Notes in Computer Science 3132.
Springer,
pp. 269–283,
doi:10.1007/978-3-540-27775-0_19.
Claudio Sacerdoti Coen (2004):
Mathematical Knowledge Management and Interactive Theorem Proving.
University of Bologna.
Gilles Dowek & Murdoch J. Gabbay (2010):
http://www.gabbay.org.uk/papers.html\#pernl-cvPermissive Nominal Logic.
In: Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2010),
pp. 165–176,
doi:10.1145/1836089.1836111.
Gilles Dowek, Murdoch J. Gabbay & Dominic P. Mulligan (2009):
http://www.gabbay.org.uk/papers.html\#perntuPermissive Nominal Terms and their Unification.
In: Proceedings of the 24th Italian Conference on Computational Logic (CILC'09).
Gilles Dowek, Murdoch J. Gabbay & Dominic P. Mulligan (2010):
http://www.gabbay.org.uk/papers.html\#perntu-jvPermissive Nominal Terms and their Unification: an infinite, co-infinite approach to nominal techniques (journal version).
Logic Journal of the IGPL 18(6),
pp. 769–822,
doi:10.1093/jigpal/jzq006.
Maribel Fernández & Murdoch J. Gabbay (2007):
http://www.gabbay.org.uk/papers.html\#curstnCurry-style types for nominal terms.
In: Types for Proofs and Programs (TYPES 06),
Lecture Notes in Computer Science 4502.
Springer,
pp. 125–139,
doi:10.1007/978-3-540-74464-1_9.
Maribel Fernández & Murdoch J. Gabbay (2007):
http://www.gabbay.org.uk/papers.html\#nomr-jvNominal rewriting (journal version).
Information and Computation 205(6),
pp. 917–965,
doi:10.1016/j.ic.2006.12.002.
Maribel Fernández & Murdoch J. Gabbay (2010):
http://www.gabbay.org.uk/papers.html\#clonreClosed nominal rewriting and efficiently computable nominal algebra equality.
In: Electronic Proceedings in Theoretical Computer Science 34,
pp. 37–51,
doi:10.4204/EPTCS.34.5.
Marcelo P. Fiore, Gordon D. Plotkin & Daniele Turi (1999):
Abstract Syntax and Variable Binding.
In: Proceedings of the 14th IEEE Symposium on Logic in Computer Science (LICS 1999).
IEEE Computer Society Press,
pp. 193–202,
doi:10.1109/LICS.1999.782615.
Murdoch J. Gabbay (2007):
http://www.gabbay.org.uk/papers.html\#frelogFresh Logic.
Journal of Applied Logic 5(2),
pp. 356–387,
doi:10.1016/j.jal.2005.10.012.
Murdoch J. Gabbay (2009):
http://www.gabbay.org.uk/papers.html\#nomahsNominal Algebra and the HSP Theorem.
Journal of Logic and Computation 19(2),
pp. 341–367,
doi:10.1093/logcom/exn055.
Murdoch J. Gabbay (2011):
http://www.gabbay.org.uk/papers.html\#fountlFoundations of nominal techniques: logic and semantics of variables in abstract syntax.
Bulletin of Symbolic Logic 17(2),
pp. 161–229,
doi:10.2178/bsl/1305810911.
Murdoch J. Gabbay (2011):
http://www.gabbay.org.uk/papers.html\#nomtnlNominal terms and nominal logics: from foundations to meta-mathematics.
In: Handbook of Philosophical Logic 17.
Kluwer.
Murdoch J. Gabbay (2011):
http://www.gabbay.org.uk/papers.html\#twolnsTwo-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables.
Mathematical Structures in Computer Science,
doi:10.1017/S0960129511000272.
Published online.
Murdoch J. Gabbay & Martin Hofmann (2008):
http://www.gabbay.org.uk/papers.html\#rensNominal renaming sets.
In: Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008).
Springer,
pp. 158–173,
doi:10.1007/978-3-540-89439-1_11.
Murdoch J. Gabbay & Stéphane Lengrand (2009):
http://www.gabbay.org.uk/papers.html\#lamcceThe lambda-context calculus (extended version).
Information and computation 207,
pp. 1369–1400,
doi:10.1016/j.ic.2009.06.004.
Murdoch J. Gabbay & Aad Mathijssen (2006):
http://www.gabbay.org.uk/papers.html\#oneaahOne-and-a-halfth-order logic.
In: Proceedings of the 8th ACM-SIGPLAN International Symposium on Principles and Practice of Declarative Programming (PPDP 2006).
ACM,
pp. 189–200,
doi:10.1145/1140335.1140359.
Murdoch J. Gabbay & Aad Mathijssen (2008):
http://www.gabbay.org.uk/papers.html\#capasn-jvCapture-Avoiding Substitution as a Nominal Algebra.
Formal Aspects of Computing 20(4-5),
pp. 451–479,
doi:10.1007/11921240_14.
Murdoch J. Gabbay & Aad Mathijssen (2008):
http://www.gabbay.org.uk/papers.html\#oneaah-jvOne-and-a-halfth-order Logic.
Journal of Logic and Computation 18(4),
pp. 521–562,
doi:10.1093/logcom/exm064.
Murdoch J. Gabbay & Aad Mathijssen (2009):
http://www.gabbay.org.uk/papers.html\#nomuaeNominal universal algebra: equational logic with names and binding.
Journal of Logic and Computation 19(6),
pp. 1455–1508,
doi:10.1093/logcom/exp033.
Murdoch J. Gabbay & Aad Mathijssen (2010):
http://www.gabbay.org.uk/papers.html\#nomalcA nominal axiomatisation of the lambda-calculus.
Journal of Logic and Computation 20(2),
pp. 501–531,
doi:10.1093/logcom/exp049.
Murdoch J. Gabbay & Andrew M. Pitts (2001):
http://www.gabbay.org.uk/papers.html\#newaas-jvA New Approach to Abstract Syntax with Variable Binding.
Formal Aspects of Computing 13(3–5),
pp. 341–363,
doi:10.1007/s001650200016.
Jean van Heijenoort (1967):
From Frege to Gödel: a source book in mathematical logic, 1879-1931.
Harvard University Press.
Leon Henkin (1950):
Completeness in the Theory of Types.
Journal of Symbolic Logic 15,
pp. 81–91.
Gueorgui I. Jojgov (2002):
Holes with Binding Power.
In: TYPES,
Lecture Notes in Computer Science 2646.
Springer,
pp. 162–181,
doi:doi:10.1007/3-540-39185-1_10.
Alexander Kurz & Daniela Petrisan (2010):
On Universal Algebra over Nominal Sets.
Mathematical Structures in Computer Science 20,
pp. 285–318,
doi:10.1017/S0960129509990399.
Karel Lambert (1963):
Existential Import Revisited.
Notre Dame Journal of Formal Logic 4(4),
pp. 288–292.
Giulio Manzonetto & Antonino Salibra (2010):
Applying Universal Algebra to Lambda Calculus.
Journal of Logic and computation 20(4),
pp. 877–915,
doi:10.1093/logcom/exn085.
Aleksandar Nanevski, Frank Pfenning & Brigitte Pientka (2008):
Contextual modal type theory.
ACM Transactions on Computational Logic (TOCL) 9(3),
pp. 1–49,
doi:10.1145/1352582.1352591.
John von Neumann (1929):
Über eine Widerspruchsfreiheitsfrage in der axiomatischen Mengenlehre.
Journal für die reine und angewandte Mathematik 160.
Lawrence C. Paulson (1989):
The Foundation of a Generic Theorem Prover.
Journal of Automated Reasoning 5(3),
pp. 363–397,
doi:10.1007/BF00248324.
Brigitte Pientka & Joshua Dunfield (2010):
Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description).
In: Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010),
Lecture Notes in Computer Science 6173.
Springer,
pp. 15–21.
Brigitte Pientka & Frank Pfenning (2003):
Optimizing Higher-Order Pattern Unification.
In: Proceedings of the 19th International Conference on Automated Deduction (CADE 2003),
Lecture Notes in Computer Science 2741.
Springer,
pp. 473–487.
Bertrand Russell (1905):
On Denoting.
Mind, New Series 14(56),
pp. 479–493.
Peter Selinger (2002):
The lambda calculus is algebraic.
Journal of Functional Programming 12(6),
pp. 549–566,
doi:10.1017/S0956796801004294.
Mark R. Shinwell, Andrew M. Pitts & Murdoch J. Gabbay (2003):
http://www.gabbay.org.uk/papers.html\#frepbmFreshML: Programming with Binders Made Simple.
In: Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP 2003) 38.
ACM Press,
pp. 263–274,
doi:10.1145/944705.944729.
Raymond Smullyan (1968):
First-order logic.
Springer.
Reprinted by Dover, 1995.
Christian Urban, Andrew M. Pitts & Murdoch J. Gabbay (2004):
http://www.gabbay.org.uk/papers.html\#nomu-jvNominal Unification.
Theoretical Computer Science 323(1–3),
pp. 473–497,
doi:10.1016/j.tcs.2004.06.016.
Pawel Urzyczyn & Morten Sørensen (2006):
Lectures on the Curry-Howard isomorphism.
Studies in Logic 149.
Elsevier.
Claus-Peter Wirth (2004):
Descente Infinie + Deduction.
Logic Journal of the IGPL 12(1),
pp. 1–96,
doi:10.1093/jigpal/12.1.1.
Julianna Zsidó (2010):
Typed abstract syntax.
University of Nice.