University of Oregon: Summer 2002 (June 24-July 5)


  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
    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
  4. Inductive Types
    • P. Martin-Lf, 1984. Intuitionistic Type Theory, Bibliopolis, Naples.
    • Th. Coquand and C. Paulin-Mohring. Inductively defined types. In P. Martin-Lf 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
  7. Computational Content of Classical Logic
  8. 8   Proof assistants

This page is the property of the University of Oregon