References

  1. 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.
  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.
  3. 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.
  4. Claudio Sacerdoti Coen (2004): Mathematical Knowledge Management and Interactive Theorem Proving. University of Bologna.
  5. 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.
  6. 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).
  7. 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.
  8. 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.
  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.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. 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.
  15. 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.
  16. 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.
  17. 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.
  18. 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.
  19. 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.
  20. 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.
  21. 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.
  22. 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.
  23. 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.
  24. 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.
  25. Jean van Heijenoort (1967): From Frege to Gödel: a source book in mathematical logic, 1879-1931. Harvard University Press.
  26. Leon Henkin (1950): Completeness in the Theory of Types. Journal of Symbolic Logic 15, pp. 81–91.
  27. 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.
  28. Alexander Kurz & Daniela Petrisan (2010): On Universal Algebra over Nominal Sets. Mathematical Structures in Computer Science 20, pp. 285–318, doi:10.1017/S0960129509990399.
  29. Karel Lambert (1963): Existential Import Revisited. Notre Dame Journal of Formal Logic 4(4), pp. 288–292.
  30. 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.
  31. 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.
  32. John von Neumann (1929): Über eine Widerspruchsfreiheitsfrage in der axiomatischen Mengenlehre. Journal für die reine und angewandte Mathematik 160.
  33. Lawrence C. Paulson (1989): The Foundation of a Generic Theorem Prover. Journal of Automated Reasoning 5(3), pp. 363–397, doi:10.1007/BF00248324.
  34. 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.
  35. 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.
  36. Bertrand Russell (1905): On Denoting. Mind, New Series 14(56), pp. 479–493.
  37. Peter Selinger (2002): The lambda calculus is algebraic. Journal of Functional Programming 12(6), pp. 549–566, doi:10.1017/S0956796801004294.
  38. 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.
  39. Raymond Smullyan (1968): First-order logic. Springer. Reprinted by Dover, 1995.
  40. 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.
  41. Pawel Urzyczyn & Morten Sørensen (2006): Lectures on the Curry-Howard isomorphism. Studies in Logic 149. Elsevier.
  42. Claus-Peter Wirth (2004): Descente Infinie + Deduction. Logic Journal of the IGPL 12(1), pp. 1–96, doi:10.1093/jigpal/12.1.1.
  43. Julianna Zsidó (2010): Typed abstract syntax. University of Nice.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org