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;
Lecturer(s)
PreviousNext 2
Lecturer
prof. dr. J.H. Geuvers
Other course modules lecturer
Lecturer
J. Jacobs, MSc
Other course modules lecturer
Lecturer
dr. R.J. Krebbers
Other course modules lecturer
Examiner
dr. F. Wiedijk
Other course modules lecturer
Contactperson for the course
dr. F. Wiedijk
Other course modules lecturer
Academic year2021
Period
KW1-KW2  (06/09/2021 to 30/01/2022)
Starting block
KW1
Course mode
full-time
Remarks-
Registration using OSIRISYes
Course open to students from other facultiesYes
Pre-registrationNo
Waiting listNo
Placement procedure-
Aims
After the course students can:
  • make type derivations in simple type theory, polymorphic type theory and dependently typed type theory
  • relate natural deduction proofs to lambda terms in these type systems
  • define simple inductive types and predicates and write functional programs using these in the Coq logic
  • modify non-dependent and non-polymorphic datatypes into their dependent and polymorphic counterparts
  • calculate the recursion principles for simple inductive types
  • use algorithm W to compute the principal type for a lambda term in simple type theory
  • prove lemmas that are part of proofs of confluence and termination for simple type theory
  • use the Coq proof assistant to make a non-trivial Coq formalization
  • understand and present a basic research paper on type theory
 
Content
This course is an introduction to type theory. Type theory studies typed versions 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. One of the main proof assistant that is based on type theory is the Coq system from INRIA in France, which is taught in the course.

Instructional Modes
  • Lectures
  • Presentations
  • Self-study
 
Level

Presumed foreknowledge
Propositional and predicate logic. Context-free grammars. Basic lambda calculus. Basic functional programming.
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 Coq formalization
  • the mark for the final written exam
Specifics
This course presupposes some maturity, both in computer science as well as in mathematics.
Required materials
Articles
One or more research articles about type theory, that also will be made available in pdf format.
Reader
Course notes written by Herman Geuvers. These course notes will be available on the website in pdf format.
Reader
Course notes written by Femke van Raamsdonk of the Free University Amsterdam. These course notes will be available on the website in pdf format.

Instructional modes
Course occurrence

Practical computer training
Attendance MandatoryYes

Tests
Exam
Test weight1
Test typeExam
OpportunitiesBlock KW2, Block KW3

Presentation
Test weight1
Test typePresentation
OpportunitiesBlock KW2, Block KW3

Coq assignment
Test weight1
Test typeAssignment
OpportunitiesBlock KW2, Block KW3

Minimum grade
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.