References

  1. Andreas Abel (2008): Normalization for the Simply-Typed Lambda-Calculus in Twelf. In: Carsten Schürmann: Proc. LFM '04, ENTCS 199. Elsevier, pp. 3–16, doi:10.1016/j.entcs.2007.11.009.
  2. Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer & Kathrin Stark (2019): POPLMark reloaded: Mechanizing proofs by logical relations. Journal of Functional Programming 29, doi:10.1017/S0956796819000170.
  3. Thorsten Altenkirch (1993): Constructions, Inductive Types and Strong Normalization. University of Edinburgh. Available at https://www.cs.nott.ac.uk/~psztxa/publ/phd93.pdf.
  4. Hendrik P. Barendregt (1985): The lambda calculus - its syntax and semantics. Studies in logic and the foundations of mathematics 103. North-Holland.
  5. Nicolaas Govert de Bruijn (1972): Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae 75(5), pp. 381–392, doi:10.1016/1385-7258(72)90034-0.
  6. Arthur Charguéraud (2012): The Locally Nameless Representation. Journal of Automated Reasoning 49(3), pp. 363–408, doi:10.1007/s10817-011-9225-2.
  7. Alonzo Church (1936): An Unsolvable Problem of Elementary Number Theory. American Journal of Mathematics 58(2), pp. 345–363, doi:10.2307/2371045.
  8. Ernesto Copello, Nora Szasz & Álvaro Tasistro (2017): Formal metatheory of the Lambda calculus using Stoughton's substitution. Theoretical Computer Science 685, pp. 65–82, doi:10.1016/j.tcs.2016.08.025.
  9. Martín Copes, Nora Szasz & Álvaro Tasistro (2018): Formalization in Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using Multiple Substitution. In: Frédéric Blanqui & Giselle Reis: Proc. LFMTP '18, EPTCS 274. Open Publishing Association, pp. 27–41, doi:10.4204/eptcs.274.3.
  10. Kevin Donnelly & Hongwei Xi (2007): A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System F. In: Alberto Momigliano & Brigitte Pientka: Proc. LFMTP '06, ENTCS 174. Elsevier, pp. 109–125, doi:10.1016/j.entcs.2007.01.021.
  11. Jean-Yves Girard, Paul Taylor & Yves Lafont (1989): Proofs and Types. Cambridge University Press.
  12. V. Kurt Gödel (1958): Über Eine Bisher Noch Nicht Benützte Erweiterung des Finiten Standpunktes. Dialectica 12(4), pp. 280–287, doi:10.1111/j.1746-8361.1958.tb01464.x.
  13. J. Roger Hindley & Jonathan P. Seldin (2008): Lambda-Calculus and Combinators: An Introduction, second edition. Cambridge University Press, doi:10.1017/CBO9780511809835.
  14. Felix Joachimski & Ralph Matthes (2003): Short proofs of normalization for the simply-typed λ-calculus, permutative conversions and Gödel's T. Archive for Mathematical Logic 42, pp. 59–87, doi:10.1007/s00153-002-0156-9.
  15. The Coq development team (2004): The Coq proof assistant reference manual. Available at http://coq.inria.fr.
  16. Ulf Norell (2007): Towards a practical programming language based on dependent type theory. Chalmers University of Technology. Available at https://www.cse.chalmers.se/~ulfn/papers/thesis.pdf.
  17. Frank Pfenning & Conal Elliott (1988): Higher-Order Abstract Syntax. In: Richard L. Wexelblat: Proc. PLDI '88. Association for Computing Machinery, pp. 199–208, doi:10.1145/53990.54010.
  18. Robert Pollack (1994): The Theory of LEGO. University of Edinburgh. Available at https://era.ed.ac.uk/handle/1842/504.
  19. Allen Stoughton (1988): Substitution revisited. Theoretical Computer Science 59(3), pp. 317–325, doi:10.1016/0304-3975(88)90149-1.
  20. William W. Tait (1967): Intensional Interpretations of Functionals of Finite Type I. The Journal of Symbolic Logic 32(2), pp. 198–212, doi:10.2307/2271658.
  21. Álvaro Tasistro, Ernesto Copello & Nora Szasz (2015): Formalisation in Constructive Type Theory of Stoughton's Substitution for the Lambda Calculus. In: Mauricio Ayala-Rincón & Ian Mackie: Proc. LSFA '14, ENTCS 312. Elsevier, pp. 215–230, doi:10.1016/j.entcs.2015.04.013.
  22. The Agda development team (2011): The Agda standard library. Available at https://github.com/agda/agda-stdlib.
  23. Christian Urban, Andrew M. Pitts & Murdoch J. Gabbay (2004): Nominal unification. Theoretical Computer Science 323(1), pp. 473–497, doi:10.1016/j.tcs.2004.06.016.
  24. Sebastián Urciuoli, Álvaro Tasistro & Nora Szasz (2020): Strong Normalization for the Simply-Typed Lambda Calculus in Constructive Type Theory Using Agda. In: Cláudia Nalon & Giselle Reis: Proc. LSFA '20, ENTCS 351. Elsevier, pp. 187–203, doi:10.1016/j.entcs.2020.08.010.
  25. Hongwei Xi (2003): Applied type system. In: Stefano Berardi, Mario Coppo & Ferruccio Damiani: Proc. TYPES '03, LNCS 3085. Springer, pp. 394–408, doi:10.1007/978-3-540-24849-1_25.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org