Type Theory and its applications in programming and document structure, a one week course in Rio Cuarto, Argentina, February 2006

Summary:

Type Theory was developed in the 70's by the Swedish mathematician Per Martin-Lof as a foundation for (constructive) mathematics. From a Computer Science perspective, it is a language in which it is possible to express both specifications and programs within the same formalism. Furthermore, the proof rules can be used to derive a correct program from a specification as well as to verify that a given program has a certain property. As a programming language, type theory is similar to typed functional languages such as ML and Haskell, but a major difference is that the evaluation of a well-typed program always terminates. The type system is using dependent types, a concept which makes it possible to identify programs and formal proofs. We can use type theory as a framework in which it is possible to express a whole range of logical formalisms. An important feature of the language is the possibility of using inductively defined sets.

The lectures will assume a general background in Mathematics and Computer Science. Some basic concepts from lambda calculus and logic is assumed. We will explain the theory and show its applications to programming and document structure.

A preliminary plan

Monday

Introduction to type theoretical ideas. slides
Brouwer, Heyting, Kolmogorov, Curry-Howard, Martin-Löf

Tuesday

Wednesday

Thursday

Friday


Some extra material:

Some suggested exercises are here.
Bengt Nordström, Department of Computing Science, Chalmers University of Technology and University of Göteborg, Sweden