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.