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
|
|
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
|
|
|
Propositional and predicate logic. Context-free grammars. Basic lambda calculus. Basic functional programming.
|
|
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
|
|
This course presupposes some maturity, both in computer science as well as in mathematics.
|
|