Next: Computer Aided Formal Reasoning Up: Contents Previous: Support

# Topics in Type Theory

This course is being held in room 5327, JCMB at 4 pm, Mondays and Wednesdays starting Monday 12th February 1996. It is arranged for the theory PG students, although others are of course welcome. The course aims to give an introduction to two central topics in the (syntactic) meta-theory of various type systems. In the first part of the course (Lectures 1-5; James McKinna), we focus on Barendregt's lambda-cube, and its generalisations known as Pure Type Systems, in order to study the problem of type-synthesis and type-checking; in the second (Lectures 6-9; Healf Goguen), we study proofs of strong normalisation using the technique of typed operational semantics, and discuss extensions of the basic functional framework of Part One to embrace inductive types and families of inductive types. There is a bibliography for the course, and there are lecture notes for the lectures on typed operational semantics and normalization for System F. Exercises will be given throughout, and the exam question will probably be a straight choice between a substantial exercise based on Part One or on Part Two.
• Lecture 1, 12 February:
Introduction. Propositions-as-types, starting from Curry's observations on S and K. Church-style typing. Martin-Löf's systems and inductive definitions. Consistency of systems for constructive mathematics. AUTOMATH and the LF. What is not considered: the Curry/ML type assignment system; intersection types; subtyping; linear types; systems of explicit substitutions; (denotational) semantics of type theory.
• Lecture 2, 14 February:
The (Pure) Calculus of Constructions, PCC, and its subsystems. The role of type dependency. Representations of logical connectives and quantifiers. Leibniz equality. Bohm-Berarducci encoding of datatypes and inductively defined predicates. Statement of Church-Rosser (CR), Subject Reduction (SR) and Strong Normalisation (SN) theorems.
• Lecture 3, 19 February:
Pure Type Systems (PTS) as a generalisation of PCC and the other systems of the cube. Predicate logics as PTSs. Basic metatheory up to SR. Problem of the lambda rule. Strengthening (proof deferred). Expansion Postponement.
• Lecture 4, 21 February:
TBA: topics in type-synthesis and type-checking for PTS.
• Lecture 5, 26 February:
TBA: topics in type-synthesis and type-checking for PTS.
• Lecture 6, 28 February:
SN. Importance of SN conceptually. Thorsten's proof of SN for (Curry-style) system F, or "Tait-style" for simply-typed lambda calculus. Differences between "Tait-style", "Girard-style" and "Martin-Löf-style" proofs. Differences between proofs for Church- and Curry-style typing. "Kripke-style".
• Lecture 7, 4 March:
Typed operational semantics (TOS). Presentation of a TOS for lambda arrow. Eta-reduction and equality and its difficulties. Strengthening and subject reduction for eta. Use of TOS to establish CR, SR, SN.
• Lecture 8, 6 March:
A TOS for PCC. Details of the normalisation proof. Equivalence with the Constructive Engine. Conversion vs. judgemental equality. Decidability of type-checking.
• Lecture 9, 11 March:
Luo's system UTT. Strict positivity. Inductive types given schematically. Finitary vs. generalised inductive definitions. Type universes. Predicativity vs. impredicativity. Extending the TOS for PCC to one for UTT.

Last updated on 23 April 1996 by Healfdene Goguen <lego@dcs.ed.ac.uk>