|This course is an introduction to type theory. Type theory studies the typed version of lambda calculus, and applies it to mathematics and computer science. It is one of the main foundations for the technology of proof assistants. In a proof assistant a mathematical proof (which often is a proof in which software or hardware is proved correct) can be developed with support from the computer in such a way that it has the highest reliability possible. The main proof assistant that is based on type theory is the Coq system from INRIA in France.|
|Course notes written by Femke van Raamsdonk of the Free University Amsterdam. These course notes will be available on the website in pdf format. One or more research articles about type theory, that also will be made available in pdf format.|
• 16 hours computer course
• 32 hours lecture
• 16 hours student presentation
• 104 hours individual study period
Extra information teaching methods: The course has two parts.
The first part consists of working through the course notes by Femke van Raamsdonk. There will be lectures and there is a practicum in which exercises will be made (there are both Coq and pen-and-paper exercises).
In the second part a more advanced topic will be studied. There will be further lectures about a reseach topic, and after that a research article will be presented in parts by the students to the group.
Besides those two parts, each participant will create a Coq formalization. Each student will have a different subject for that formalization.
The practicum will use the ProofWeb system, which allows students to use the Coq proof assistant through the web. If there are only a few students, the practicum will not be given as contact hours, but instead there will be regular meetings for feedback.
|This course is interesting for mathematics students.|
|• the Coq proof assistant|
• the type system lambda-arrow: simple type theory, simply typed lambda calculus
• the type system lambda-P: dependent types and logical frameworks
• the type system lambda-2: polymorphism and second order propositional logic
• Pure Type Systems in general and the Barendregt cube
• the Curry-Howard-de Bruijn isomorphism
• classical versus intuitionistic logic
• the type checking and inhabitation problems
• term normalization, detour elimination, and their relation
• inductive types and predicates, recursive functions
• program extraction
• a more advanced research topic
|The final note will be the average of three marks:|
• the mark for the presentation in the second part of the course
• the mark for the final written exam
• the mark for the Coq formalization
There is a deadline for handing in the Coq exercise. If this deadline is not met, the Coq exercise will be considered not to have been made.
|Basic lambda calculus. Functional programming.|