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:
-
walf
An earlier implementation by Lena Magnusson and Johan Nordlander. Supports
inductive definition of families of sets.
-
alfa
An implementation by Thierry Couquand and Thomas Hallgren. Supports pattern
matching, sigma types, ...
-
half The same proof engine as alfa, but uses an emacs-interface
written by Dan Synek. You can contact him for more information.
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