Type Theory and Programming, a one week course

This one week course is one out of seven weeks of introduction to Computing Science research at the department of Computing Science in Göteborg. The course is  planned as an introduction to new graduate students, but anyone who is interested is welcome. For a complete description of the other weeks see  the URL http://www.cs.chalmers.se/~makoto/obligpg.html.

Logical frameworks based on type theory have been developed at INRIA in Paris (COQ), University of Edinburgh (LF and Lego) and at Chalmers (ALF). The goal behind a logical framework is to have a language in which many different logical theories can be expressed. The user should state the axioms and rules and the framework gives then an interactive proof system for that particular logic. One of the primary goals is that the systems should be used for program development. This is an area where machine-aided verification could become important, real programs are long and proofs about them contains many details which have to be checked.

In this course we will give a short introduction to ALF and the theory behind it (Martin-Lof's monomorphic type theory). We will give examples of theories from logic and mathematics (propositional logic, predicate logic, arithmetics) and from computing (theories of lists and other inductively defined sets).

There are some implementations of (versions of) Martin-Lof's logical framework currently available:

A preliminary plan

Each day has the same schedule. There will be a lecture at 10.15 - 12.00 and then a discussion session 13.15 - 15.00. The following gives a coarse description of the lectures, it will probably be changed!

Monday

A fundamental idea in type theory is the identification between types, propositions and specifications of programs (and similarly objects, proofs and programs). This is not just a formal coincident. I will talk about propositions as types and Heyting's and Kolmogoroff's explanation of the logical constants.

A formalization of propositonal logic in ALF, an introduction to the computer implementation.

Tuesday

Martin-Löf's type theory. Different judgement forms. Comparision between type theory and a typed functional programming language.

Wednesday

Propositional logic and predicate logic in type theory. The monomorphic set theory. Formation-, introduction-, elimination- and equality rules. The induction schemes expressed in the elimination rules.

Thursday

How to express lists and other inductively defined sets used in programming. How to define predicates and relations.

Friday

In the morning we will have a a question-answer period and in the afternoon there will be a short written examination. I try to make the questions so that they are very easy ( almost trivial) to answer if you have understood my lectures. 

Some written material which we are going to use:

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