Type Theory

• Type Theory: Impredicative Part, by Alexandre Miquel, 3 - 7 March.
• Dependent Type Theory, by Thierry Coquand and Peter Dybjer.
• Interactive theorem proving with Alfa, by Marcin Benke.

Type Theory: Impredicative Part

1. System F (Church & Curry)
2. The erasing function; second-order quantification as an intersection
3. The strong normalisation theorem
4. Normalisation of HA2 and consistency
5. System Fw and Church's theory of simple types
6. Inconsistent extensions (system U, *:*) : the failure of parametricity

Dependent Type Theory

1. Friday 14 March, 13.15 - 15.00 in S4. Introduction (Thierry Coquand). Slides
   • Historical remarks
   • NuPurl, Coq, Alfa
   • What we can hope from type theory: applications, certificate, computer algebra, polytyping, formalised documents
   • Reading: Martin-Löf 1972. (See list below)
2. Friday 21 March, 10.15 - 12.00 in Hörsalen. The logical framework (Thierry Coquand). Slides
   • Simply typed lambda calculus
   • Church's higher order logic
   • Isabelle
   • Lambda calculus with dependent types
   • Records
3. Friday 4 April, 10.15 - 12.00 in S4. Logic (Peter Dybjer)
   • Logical connectives
   • Quantifiers
   • Representation in Church's higher-order logic
   • Representation in logical framework
   • Representation of proofs in natural deduction
   • Meaning explanations, BHK-semantics, importance of canonical forms
4. Friday 11 April, 10.15 - 12.00 in S2. Inductive and recursive definitions (Peter Dybjer).
   • Natural numbers, representation of Peano's axioms in type theory
   • Equality
5. Friday 25 April, 10.15 - 12.00 in S2. Inductive and recursive definitions, continued (Peter Dybjer)
   • More on equality and the Peano axioms
   • Gödel System T
   • Universes
   • Algebraic datatypes
   • Infinitary induction
6. Friday 9 May, 10.15 - 12.00 in S2. Inductive and recursive definitions, continued (Peter Dybjer).
   • Inductive families and predicates
   • Well-founded relations
   • The Church-Rosser property (Birger Nordborg)
7. Friday 23 May, 10.15 in S2.
   • A per-model of dependent type theory (Pierre Hyvernat)

Examination

1. The first alternative consists of two parts:
   • Give a 30-45 minute presentation of some paper in dependent type theory;
   • Hand in solutions to some exercises.
2. Write a type-checker for dependent type theory with V:V in Haskell.

Reading

• Martin-Löf, Per, An Intuitionistic Theory of Types, in Twenty-Five Years of Constructive Type Theory, eds G. Sambin and J. Smith, Oxford University Press, 1998 (reprinted version of an unpublished report from 1972).
• Martin-Löf, Per, On the meaning of the logical constants and the justification of the logical laws, short course given at the meeting Teoria della Dimostrazione e Filosofia della Logica, organized in Siena, 6-9 April 1983, by the Scuola di Specializzazione in Logica Matematica of the Università degli Studi di Siena.
• Church, Alonzo, A formulation of the simple theory of types. J. Symbolic logic 5, (1940). 56--68.
• Harper, Robert; Honsell, Furio; Plotkin, Gordon=20 A framework for defining logics. J. Assoc. Comput. Mach. 40 (1993), no. 1, 143--184.
• Gödel, Kurt, On a hitherto unexploited extension of the finitary standpoint. in Collected works. Vol. II. Publications 1938--1974.=20 The Clarendon Press, Oxford University Press, New York, 1990.

Books

• Intuitionistic Type Theory, by Per Martin-Löf, Bibliopolis 1984.
• Programming in Martin-Löf's Type Theory - an Introduction, by Bengt Nordström, Kent Petersson, and Jan Smith, Oxford University Press 1989.
• Proofs and Types, by Jean-Yves Girard, Yves Lafont, and Paul Taylor, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press 1989.

Other

• Testing and the meaning of the judgements of Martin-Löf type theory, Peter's answer to a question by Andy Fugard