Entry requirements

120 credit points and Logic II or Applied Logic

Learning outcomes

In order to pass the course (grade 3) the student should

• master lambda calculus and type inference;
• be able to give an account of the main lines in the proofs for confluence and normalisation for a typed lambda calculus;
• be familiar with algorithmic interpretation of logic;
• be able to carry out formal proofs in type theory and logical systems based on intuitionistic logic;
• know the basics and principles of constructive mathematics;
• be able to motivate type constructions through informal meaning explanations;
• know the most important metamathematical properties of type theories.

Content

Lambda calculus: untyped lambda calculus, reduction and conversion. Church–Rosser property, normal forms, Church numerals and representation of recursive functions. Lazy and eager evaluation. Böhm trees. Typed lambda calculus: type inference, type constructions. Dependent types. Strong and weak normalisation. Models of lambda calculus.

Type theory: contexts, context maps, judgement forms, meaning explanations, the BHK-interpretation. Dependent products and sums. Inductive types. Identity types. Type universes. Inductively recursive types. Proof-theoretic properties and models of type theory. Logical frameworks.

Constructive mathematics in type theory: sets as types with equivalence relations. Properties of set theory. Intuitionistic logic. Examples from constructive mathematics: algebra, analysis and topology. Executable proofs.

Instruction

Lectures and problem solving sessions.

Assessment

Written examination at the end of the course combined with assignments given during the course.