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 1
Lecturer
prof. dr. J.H. Geuvers
Other course modules lecturer
Lecturer
dr. R.J. Krebbers
Other course modules lecturer
Lecturer
dr. F. Wiedijk
Other course modules lecturer
Examiner
dr. F. Wiedijk
Other course modules lecturer
Coordinator
dr. F. Wiedijk
Other course modules lecturer
Academic year2020
Period
KW1-KW2  (31/08/2020 to 24/01/2021)
Starting block
KW1
Course mode
full-time
RemarksThis course has been moved to Q1+2
Registration using OSIRISYes
Course open to students from other facultiesYes
Pre-registrationNo
Waiting listNo
Placement procedure-
Aims
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
Content
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.

Instructional Modes
  • Lecture
  • Presentation
  • Self-study
Level

Presumed foreknowledge
Basic lambda calculus. 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 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.
  • Specifics
    This course is interesting for mathematics students.
    Required materials
    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.

    Recommended materials
    Articles
    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

    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.