Bibliography

1. Logic
   • J.-Y. Girard, Y. Lafont, P. Taylor Proofs and Types,Cambridge University Press
   • Troelstra, A.S and D. van Dalen, Constructivism in mathematics, an introduction, two volumes, North-Holland, 1988.
2. Type Systems
   1. General
      • M.H. Sorensen, P. Urzyczyn, Lectures on the Curry-Howard Isomorphism
      • H. Barendregt, Lambda calculus with types,in: Handbook of Theoretical Computer Science, Elsevier (1990), 323-363.
      • J.H. Geuvers, Logics and Type systems, PhD. Thesis, University of Nijmegen, September 1993
   2. Exercises
      • Henk Barendregt, Problems in type theory In: Computational Logic, U. Berger and H. Schwichtenberg (eds.), Springer (1999), pp. 99--112.
3. Proof-Carrying Code
   • The Fox project on Proof-Carrying Code
   • G. Necula's page on Proof-Carrying Code
   • Proof-Carrying Code at the Secure Internet Programming page
4. Inductive Types
   • P. Martin-Löf, 1984. Intuitionistic Type Theory, Bibliopolis, Naples.
   • Th. Coquand and C. Paulin-Mohring. Inductively defined types. In P. Martin-Löf and G. Mints, editors, Proceedings of Colog'88, volume 417 of Lecture Notes in Computer Science. Springer-Verlag, 1990.
5. Decidability of Unification, Pattern-Matching, Type-Checking and Type Inference
   • G. Huet: A Unification Algorithm for Typed lambda-Calculus. TCS 1(1): 27-57 (1975) is an excellent paper.
   • F. Goldfarb. The undecidability of the second-order unification problem. Journal of Theoretical Computer Science, 13:225--230, 1981.
   • F. Pfenning's page on Logical Frameworks, Implementation, Theorem Proving
6. Realisability and Extraction
   • L. Boerio, Optimizing Programs Extracted from Proofs, PhD thesis.
   • S. Berardi, M. Coppo, F. Damiani, Type-based useless code elimination for functional programs, SAIG'00.
   • F. Damiani and P. Giannini. Automatic useless-code detection and elimination for hot functional programs Journal of Functional Programming, 10(6):509-559, 2000.
7. Computational Content of Classical Logic
   • T. Griffin, A formulae-as-types notion of control, POPL'90.
   • A. Sabry and M. Felleisen. Reasoning about programs in cps-style, Lisp and symbolic computation 6, 1993.
   • A. Sabry and P. Wadler. A Reflection on Call-by-Value, In the ACM SIGPLAN International Conference on Functional Programming, 13-24. ACM Press, New York, 1996.
   • T. Coquand, , Computational content of classical logic, lecture notes for a course given in Cambridge, 1995.
   • M. Parigot, lµ-calculus: An Algorithmic interpretation of classical natural deduction, LPAR'92.
   • F. Barbanera and S. Berardi, A Symmetric l-Calculus for ``Classical'' Program Extraction, Information and Computation 125, 1996.
   • P.-L. Curien and H. Herbelin, The Duality of Computation, ICFP'00.
8. 8   Proof assistants
   • The Coq Proof Assistant
   • The PVS Prover
   • HOL-Light
   • The Twelf Logical Framework
   • Carolyn Talcott's page on Mechanized Reasoning