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