 After the course students can:
 explain the notions in the subjects list below
 make type derivations in the type systems lambdaarrow, lambdaP and lambda2
 translate natural deduction proofs to lambda terms in these type systems, and vice versa
 relate detours to term redexes and eliminate detours from natural deduction proofs
 give the detours for the various logical connectives
 define simple inductive types and predicates and write functional programs in the Coq logic on them
 calculate the recursion principles for simple inductive types
 modify nondependent and nonpolymorphic datatypes into their dependent and polymorphic counterparts
 use lambdaP as a logical framework for a simple logic
 use the Coq proof assistant to make a nontrivial Coq formalization
 understand and present a basic research paper on type theory

 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 penandpaper 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 lambdaarrow: simple type theory, simply typed lambda calculus • the type system lambdaP: dependent types and logical frameworks • the type system lambda2: polymorphism and second order propositional logic • Pure Type Systems in general and the Barendregt cube • the CurryHowardde 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. 
  Required materialsReaderCourse notes written by Femke van Raamsdonk of the Free University Amsterdam. These course notes will be available on the website in pdf format. 

 Recommended materialsArticlesOne or more research articles about type theory, that also will be made available in pdf format. 

 Instructional modesCourse occurrence
 Lecture
 Practical computer trainingAttendance Mandatory   Yes 
 PresentationAttendance Mandatory   Yes 
 Zelfstudie

 TestsTentamenTest weight   1 
Opportunities   Block KW4, Block KW4 


 