@inbook(asperti:crafting:2007,
 author       = "Andrea Asperti and Claudo~Sacerdoti Coen and Enrico Tassi and Stefano Zacchiroli",
 year         = "2007",
 title        = "Crafting a Proof Assistant",
 pages        = "18--32",
 series       = "Lecture Notes in Computer Science",
 publisher    = "Springer",
 doi          = "10.1007/978-3-540-74464-1\_2",
)
@article(benzmuller:higose,
 author       = "Christoph Benzm{\"u}ller and Chad~E. Brown and Michael Kohlhase",
 year         = "2004",
 title        = "Higher-order semantics and extensionality",
 journal      = "Journal of Symbolic Logic",
 volume       = "69",
 pages        = "1027--1088",
 doi          = "10.2178/jsl/1102022211",
)
@inproceedings(cheney:alppl,
 author       = "James Cheney and Christian Urban",
 year         = "2004",
 title        = "Alpha-Prolog: A Logic Programming Language with Names, Binding and Alpha-Equivalence",
 editor       = "Bart Demoen and Vladimir Lifschitz",
 booktitle    = "Proceedings of the 20th International Conference on Logic Programming (ICLP 2004)",
 series       = "Lecture Notes in Computer Science",
 volume       = "3132",
 publisher    = "Springer",
 pages        = "269--283",
 doi          = "10.1007/978-3-540-27775-0\_19",
)
@phdthesis(sacerdoti:thesis,
 author       = "Claudio~Sacerdoti Coen",
 year         = "2004",
 title        = "Mathematical Knowledge Management and Interactive Theorem Proving",
 school       = "University of Bologna",
)
@inproceedings(gabbay:pernl,
 author       = "Gilles Dowek and Murdoch~J. Gabbay",
 year         = "2010",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#pernl-cv}{Permissive Nominal Logic}",
 booktitle    = "Proceedings of the 12th International {ACM} {SIGPLAN} Symposium on Principles and Practice of Declarative Programming ({PPDP} 2010)",
 pages        = "165--176",
 doi          = "10.1145/1836089.1836111",
)
@inproceedings(gabbay:perntu,
 author       = "Gilles Dowek and Murdoch~J. Gabbay and Dominic~P. Mulligan",
 year         = "2009",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#perntu}{Permissive Nominal Terms and their Unification}",
 booktitle    = "Proceedings of the 24th Italian Conference on Computational Logic (CILC'09)",
)
@article(gabbay:perntu-jv,
 author       = "Gilles Dowek and Murdoch~J. Gabbay and Dominic~P. Mulligan",
 year         = "2010",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#perntu-jv}{Permissive Nominal Terms and their Unification: an infinite, co-infinite approach to nominal techniques (journal version)}",
 journal      = "Logic Journal of the {IGPL}",
 volume       = "18",
 number       = "6",
 pages        = "769--822",
 doi          = "10.1093/jigpal/jzq006",
)
@incollection(gabbay:curstn,
 author       = "Maribel Fern{\'a}ndez and Murdoch~J. Gabbay",
 year         = "2007",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#curstn}{Curry-style types for nominal terms}",
 booktitle    = "Types for Proofs and Programs ({TYPES} 06)",
 series       = "Lecture Notes in Computer Science",
 volume       = "4502",
 publisher    = "Springer",
 pages        = "125--139",
 doi          = "10.1007/978-3-540-74464-1\_9",
)
@article(gabbay:nomr-jv,
 author       = "Maribel Fern{\'a}ndez and Murdoch~J. Gabbay",
 year         = "2007",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#nomr-jv}{Nominal rewriting (journal version)}",
 journal      = "Information and Computation",
 volume       = "205",
 number       = "6",
 pages        = "917--965",
 doi          = "10.1016/j.ic.2006.12.002",
)
@inproceedings(gabbay:clonre,
 author       = "Maribel Fern{\'a}ndez and Murdoch~J. Gabbay",
 year         = "2010",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#clonre}{Closed nominal rewriting and efficiently computable nominal algebra equality}",
 booktitle    = "Electronic Proceedings in Theoretical Computer Science",
 volume       = "34",
 pages        = "37--51",
 doi          = "10.4204/EPTCS.34.5",
)
@inproceedings(fiore:abssvb,
 author       = "Marcelo~P. Fiore and Gordon~D. Plotkin and Daniele Turi",
 year         = "1999",
 title        = "Abstract Syntax and Variable Binding",
 booktitle    = "Proceedings of the 14th {IEEE} Symposium on Logic in Computer Science ({LICS} 1999)",
 publisher    = "IEEE Computer Society Press",
 pages        = "193--202",
 doi          = "10.1109/LICS.1999.782615",
)
@article(gabbay:frelog,
 author       = "Murdoch~J. Gabbay",
 year         = "2007",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#frelog}{{F}resh {L}ogic}",
 journal      = "Journal of Applied Logic",
 volume       = "5",
 number       = "2",
 pages        = "356--387",
 doi          = "10.1016/j.jal.2005.10.012",
)
@article(gabbay:nomahs,
 author       = "Murdoch~J. Gabbay",
 year         = "2009",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#nomahs}{Nominal Algebra and the {HSP} Theorem}",
 journal      = "Journal of Logic and Computation",
 volume       = "19",
 number       = "2",
 pages        = "341--367",
 doi          = "10.1093/logcom/exn055",
)
@article(gabbay:fountl,
 author       = "Murdoch~J. Gabbay",
 year         = "2011",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#fountl}{Foundations of nominal techniques: logic and semantics of variables in abstract syntax}",
 journal      = "Bulletin of Symbolic Logic",
 volume       = "17",
 number       = "2",
 pages        = "161--229",
 doi          = "10.2178/bsl/1305810911",
)
@incollection(gabbay:nomtnl,
 author       = "Murdoch~J. Gabbay",
 year         = "2011",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#nomtnl}{Nominal terms and nominal logics: from foundations to meta-mathematics}",
 booktitle    = "Handbook of Philosophical Logic",
 volume       = "17",
 publisher    = "Kluwer",
)
@article(gabbay:twolns,
 author       = "Murdoch~J. Gabbay",
 year         = "2011",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#twolns}{Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables}",
 journal      = "Mathematical Structures in Computer Science",
 doi          = "10.1017/S0960129511000272",
 note         = "Published online",
)
@inproceedings(gabbay:nomrs,
 author       = "Murdoch~J. Gabbay and Martin Hofmann",
 year         = "2008",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#rens}{Nominal renaming sets}",
 booktitle    = "Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning ({LPAR} 2008)",
 publisher    = "Springer",
 pages        = "158--173",
 doi          = "10.1007/978-3-540-89439-1\_11",
)
@article(gabbay:lamcce,
 author       = "Murdoch~J. Gabbay and St{\'e}phane Lengrand",
 year         = "2009",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#lamcce}{The lambda-context calculus (extended version)}",
 journal      = "Information and computation",
 volume       = "207",
 pages        = "1369--1400",
 doi          = "10.1016/j.ic.2009.06.004",
)
@inproceedings(gabbay:oneaah,
 author       = "Murdoch~J. Gabbay and Aad Mathijssen",
 year         = "2006",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#oneaah}{One-and-a-halfth-order logic}",
 booktitle    = "Proceedings of the 8th {ACM-SIGPLAN} International Symposium on Principles and Practice of Declarative Programming ({PPDP} 2006)",
 publisher    = "ACM",
 pages        = "189--200",
 doi          = "10.1145/1140335.1140359",
)
@article(gabbay:capasn-jv,
 author       = "Murdoch~J. Gabbay and Aad Mathijssen",
 year         = "2008",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#capasn-jv}{Capture-Avoiding Substitution as a Nominal Algebra}",
 journal      = "Formal Aspects of Computing",
 volume       = "20",
 number       = "4-5",
 pages        = "451--479",
 doi          = "10.1007/11921240\_14",
)
@article(gabbay:oneaah-jv,
 author       = "Murdoch~J. Gabbay and Aad Mathijssen",
 year         = "2008",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#oneaah-jv}{One-and-a-halfth-order Logic}",
 journal      = "Journal of Logic and Computation",
 volume       = "18",
 number       = "4",
 pages        = "521--562",
 doi          = "10.1093/logcom/exm064",
)
@article(gabbay:nomuae,
 author       = "Murdoch~J. Gabbay and Aad Mathijssen",
 year         = "2009",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#nomuae}{Nominal universal algebra: equational logic with names and binding}",
 journal      = "Journal of Logic and Computation",
 volume       = "19",
 number       = "6",
 pages        = "1455--1508",
 doi          = "10.1093/logcom/exp033",
)
@article(gabbay:nomalc,
 author       = "Murdoch~J. Gabbay and Aad Mathijssen",
 year         = "2010",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#nomalc}{A nominal axiomatisation of the lambda-calculus}",
 journal      = "Journal of Logic and Computation",
 volume       = "20",
 number       = "2",
 pages        = "501--531",
 doi          = "10.1093/logcom/exp049",
)
@article(gabbay:newaas-jv,
 author       = "Murdoch~J. Gabbay and Andrew~M. Pitts",
 year         = "2001",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#newaas-jv}{A New Approach to Abstract Syntax with Variable Binding}",
 journal      = "Formal Aspects of Computing",
 volume       = "13",
 number       = "3--5",
 pages        = "341--363",
 doi          = "10.1007/s001650200016",
)
@book(heijenoort:fregsb,
 author       = "Jean van Heijenoort",
 year         = "1967",
 title        = "From Frege to G\"odel: a source book in mathematical logic, 1879-1931",
 publisher    = "Harvard University Press",
)
@article(henkin:comtot,
 author       = "Leon Henkin",
 year         = "1950",
 title        = "Completeness in the Theory of Types",
 journal      = "Journal of Symbolic Logic",
 volume       = "15",
 pages        = "81--91",
)
@inproceedings(jojgov:holbp,
 author       = "Gueorgui~I. Jojgov",
 year         = "2002",
 title        = "Holes with Binding Power",
 booktitle    = "TYPES",
 series       = "Lecture Notes in Computer Science",
 volume       = "2646",
 publisher    = "Springer",
 pages        = "162--181",
 doi          = "doi:10.1007/3-540-39185-1\_10",
)
@article(kurz:unians,
 author       = "Alexander Kurz and Daniela Petri\c {s}an",
 year         = "2010",
 title        = "On Universal Algebra over Nominal Sets",
 journal      = "Mathematical Structures in Computer Science",
 volume       = "20",
 pages        = "285--318",
 doi          = "10.1017/S0960129509990399",
)
@article(lambert:exiir,
 author       = "Karel Lambert",
 year         = "1963",
 title        = "Existential Import Revisited",
 journal      = "Notre Dame Journal of Formal Logic",
 volume       = "4",
 number       = "4",
 pages        = "288--292",
)
@article(salibra:appual,
 author       = "Giulio Manzonetto and Antonino Salibra",
 year         = "2010",
 title        = "Applying Universal Algebra to Lambda Calculus",
 journal      = "Journal of Logic and computation",
 volume       = "20",
 number       = "4",
 pages        = "877--915",
 doi          = "10.1093/logcom/exn085",
)
@article(nanevski:conmtt,
 author       = "Aleksandar Nanevski and Frank Pfenning and Brigitte Pientka",
 year         = "2008",
 title        = "Contextual modal type theory",
 journal      = "ACM Transactions on Computational Logic (TOCL)",
 volume       = "9",
 number       = "3",
 pages        = "1--49",
 doi          = "10.1145/1352582.1352591",
)
@article(vonneumann:ubewam,
 author       = "John von Neumann",
 year         = "1929",
 title        = "\"{U}ber eine {W}iderspruchsfreiheitsfrage in der axiomatischen {M}engenlehre",
 journal      = "Journal f\"{u}r die reine und angewandte {M}athematik",
 volume       = "160",
)
@article(PaulsonLC:fougtp,
 author       = "Lawrence~C. Paulson",
 year         = "1989",
 title        = "The Foundation of a Generic Theorem Prover",
 journal      = "Journal of Automated Reasoning",
 volume       = "5",
 number       = "3",
 pages        = "363--397",
 doi          = "10.1007/BF00248324",
)
@inproceedings(pientka:belfpr,
 author       = "Brigitte Pientka and Joshua Dunfield",
 year         = "2010",
 title        = "Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)",
 booktitle    = "Proceedings of the 5th International Joint Conference on Automated Reasoning ({IJCAR} 2010)",
 series       = "Lecture Notes in Computer Science",
 volume       = "6173",
 publisher    = "Springer",
 pages        = "15--21",
)
@inproceedings(pientka:opthop,
 author       = "Brigitte Pientka and Frank Pfenning",
 year         = "2003",
 title        = "Optimizing Higher-Order Pattern Unification",
 booktitle    = "Proceedings of the 19th International Conference on Automated Deduction ({CADE} 2003)",
 series       = "Lecture Notes in Computer Science",
 volume       = "2741",
 publisher    = "Springer",
 pages        = "473--487",
)
@article(russell:ond,
 author       = "Bertrand Russell",
 year         = "1905",
 title        = "On Denoting",
 journal      = "Mind, New Series",
 volume       = "14",
 number       = "56",
 pages        = "479–493",
)
@article(selinger:lamca,
 author       = "Peter Selinger",
 year         = "2002",
 title        = "The lambda calculus is algebraic",
 journal      = "Journal of Functional Programming",
 volume       = "12",
 number       = "6",
 pages        = "549--566",
 doi          = "10.1017/S0956796801004294",
)
@inproceedings(gabbay:frepbm,
 author       = "Mark~R. Shinwell and Andrew~M. Pitts and Murdoch~J. Gabbay",
 year         = "2003",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#frepbm}{Fresh{ML}: Programming with Binders Made Simple}",
 booktitle    = "Proceedings of the 8th {ACM} {SIGPLAN} International Conference on Functional Programming ({ICFP} 2003)",
 volume       = "38",
 publisher    = "ACM Press",
 pages        = "263--274",
 doi          = "10.1145/944705.944729",
)
@book(smullyan:firol,
 author       = "Raymond Smullyan",
 year         = "1968",
 title        = "First-order logic",
 publisher    = "Springer",
 note         = "Reprinted by Dover, 1995",
)
@article(gabbay:nomu-jv,
 author       = "Christian Urban and Andrew~M. Pitts and Murdoch~J. Gabbay",
 year         = "2004",
 title        = "\href {http://www.gabbay.org.uk/papers.html\#nomu-jv}{Nominal Unification}",
 journal      = "Theoretical Computer Science",
 volume       = "323",
 number       = "1--3",
 pages        = "473--497",
 doi          = "10.1016/j.tcs.2004.06.016",
)
@book(sorensen:lecchi-book,
 author       = "Pawel Urzyczyn and Morten S{\o }rensen",
 year         = "2006",
 title        = "Lectures on the Curry-Howard isomorphism",
 series       = "Studies in Logic",
 volume       = "149",
 publisher    = "Elsevier",
)
@article(Wirth:desid,
 author       = "Claus-Peter Wirth",
 year         = "2004",
 title        = "Descente Infinie + {D}eduction",
 journal      = "Logic Journal of the IGPL",
 volume       = "12",
 number       = "1",
 pages        = "1--96",
 doi          = "10.1093/jigpal/12.1.1",
)
@phdthesis(zsido:typas,
 author       = "Julianna Zsid\'o",
 year         = "2010",
 title        = "Typed abstract syntax",
 school       = "University of Nice",
)