Entry requirements

120 credits and Logic II or Applied Logic. Proficiency in English equivalent to the Swedish upper secondary course English 6.

Learning outcomes

On completion of the course, the student should be able to:

• 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.

If there are special reasons for doing so, an examiner may make an exception from the method of assessment indicated and allow a student to be assessed by another method. An example of special reasons might be a certificate regarding special pedagogical support from the disability coordinator of the university.