Kies de Nederlandse taal
Course module: NWI-IMC010
Type Theory and Coq
Course infoSchedule
Course moduleNWI-IMC010
Credits (ECTS)6
CategoryMA (Master)
Language of instructionEnglish
Offered byRadboud University; Faculty of Science; Informatica en Informatiekunde;
prof. dr. J.H. Geuvers
Other course modules lecturer
dr. F. Wiedijk
Other course modules lecturer
dr. F. Wiedijk
Other course modules lecturer
Contactperson for the course
dr. F. Wiedijk
Other course modules lecturer
Academic year2017
KW3-KW4  (05/02/2018 to 02/09/2018)
Starting block
Course mode
Registration using OSIRISYes
Course open to students from other facultiesYes
Waiting listNo
Placement procedure-

After the course students can:

  • explain the notions in the subjects list below
  • make type derivations in the type systems lambda-arrow, lambda-P and lambda-2
  • 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 non-dependent and non-polymorphic datatypes into their dependent and polymorphic counterparts
  • use lambda-P as a logical framework for a simple logic
  • use the Coq proof assistant to make a non-trivial 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.
Teaching formats

• 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.
Additional comments
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
Test information
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 materials
Course notes written by Femke van Raamsdonk of the Free University Amsterdam. These course notes will be available on the website in pdf format.
Recommended materials
One or more research articles about type theory, that also will be made available in pdf format.
Instructional modes
Course occurrence


Practical computer training
Attendance MandatoryYes

Attendance MandatoryYes


Test weight1
OpportunitiesBlock KW4, Block KW4

Kies de Nederlandse taal