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 be able to

  • give an account of important concepts and definitions in the area of the course;

  • exemplify and interpret important concepts in specific cases;

  • formulate important results and theorems covered by the course;

  • describe the main features of the proofs of important theorems;

  • express problems from relevant areas of applications in a mathematical form suitable for further analysis;

  • use the theory, methods and techniques of the course to solve mathematical problems;

  • present mathematical arguments to others.

    Higher grades, 4 or 5, require a higher level of proficiency. The student should be able to solve problems of greater complexity, i.e. problems requiring a combination of ideas and methods for their solution, and be able to give a more detailed account of the proofs of important theorems and by examples and counter-examples be able to motivate the scope of various results. Requirements concerning the student's ability to present mathematical arguments and reasoning are greater.

    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.