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) metatheory of various type systems. In the first part of
the course (Lectures 15; James McKinna), we focus on Barendregt's
lambdacube, and its generalisations known as Pure Type Systems, in
order to study the problem of typesynthesis and typechecking; in the
second (Lectures 69; 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. Propositionsastypes, starting from Curry's
observations on S and K. Churchstyle typing. MartinLö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.
BohmBerarducci encoding of datatypes and inductively defined
predicates. Statement of ChurchRosser (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 typesynthesis and typechecking for PTS.

Lecture 5, 26 February:
TBA: topics in typesynthesis and typechecking for PTS.

Lecture 6, 28 February:
SN. Importance of SN conceptually. Thorsten's proof of SN
for (Currystyle) system F, or "Taitstyle" for simplytyped
lambda calculus. Differences between "Taitstyle",
"Girardstyle" and "MartinLöfstyle" proofs. Differences
between proofs for Church and Currystyle typing.
"Kripkestyle".

Lecture 7, 4 March:
Typed operational semantics (TOS). Presentation of a TOS
for lambda arrow. Etareduction 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 typechecking.

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>