Type Theory Course


  1. Motivation, background. Kolmogorov's and Heyting's explanations of the logical constants.
  2. An overview of the polymorhic type theory. This is an obsolete theory which is a historical stepping stone towards the monomorphic theory. Syntax: the theory of expressions with their arities. Semantics of the different judgement forms. Structure of the formal system.
  3. The cartesian product between two sets and the disjoint union of a family of sets. Different reading of the rules. Enumeration sets.
  4. Natural numbers. The cartesian product of a family of sets and its special cases (the for all quantifier, the set of functions, implication). Propositional equality.
  5. A brief overview of the monomorphic theory. Types and objects. Definitions. How to represent a proof. How to build a proof.
  6. The compiler example.
  7. Universes and wellorderings. How to express different inductive sets using wellorderings and the problem with intensional equality. Peano's fourth axiom.
  8. The relationship between Alfa and typetheory.

Some exercises.

Examination questions

Bengt Nordstr|m

Fri Sep 5 13:39:35 MET DST 1997