Type Theory and Lambda Calculus

10 credits

Syllabus, Master's level, 1MA059

A revised version of the syllabus is available.
Code
1MA059
Education cycle
Second cycle
Main field(s) of study and in-depth level
Mathematics A1F
Grading system
Pass with distinction (5), Pass with credit (4), Pass (3), Fail (U)
Finalised by
The Faculty Board of Science and Technology, 15 March 2007
Responsible department
Department of Mathematics
What is a course syllabus?

Entry requirements

BSc, 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 and, possibly, oral examination at the end of the course. Moreover, compulsory assignments may be given during the course.