Type Theory

Course manual 2023/2024

Course content

Type theory is a subject which lies at the intersection of mathematics, logic and computer science. In this course the emphasis will be on how type theory can be used as a framework for developing mathematics and verifying mathematical proofs. We will discuss various version of the lambda calculus (untyped, simply typed, second order typed and dependently typed). The course will culminate in the Calculus of Constructions (CoC) and investigate how that provides a setting for formalising mathematics.

Study materials

Literature

• M.H. Soerensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Elsevier, 2006.

Objectives

• Encode mathematical proofs in type theory
• Prove properties about type theories

Teaching methods

• Lecture
• Computer lab session/practical training

Learning activities

Attendance

This programme does not have requirements concerning attendance (TER-B).

Assessment

The grade for the course for the course is determined by homework assignments (which count for 30%) and a written exam (which counts for 70%). The grade for the written exam needs to be at least 5. The same rules apply for the resit.

Inspection of assessed work

Via Canvas.

Assignments

Homework assignments are submitted individually and each student has to write their own solutions. Solutions are submitted throught Canvas, where they are also graded and where the students receive feedback on their work.

Fraud and plagiarism

The 'Regulations governing fraud and plagiarism for UvA students' applies to this course. This will be monitored carefully. Upon suspicion of fraud or plagiarism the Examinations Board of the programme will be informed. For the 'Regulations governing fraud and plagiarism for UvA students' see: www.student.uva.nl

Course structure

Additional information

There will be a Canvas page for the course.

Contact information

Coordinator

• B. van den Berg

Staff

• Daniël Otten MSc