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
- Judgements and propositions
- Judgement forms
- Semantics of the different judgement forms
- Polymorphic theory vs monomorphic theory
- Brief overview of the polymorphic theory:
- Introduction, elimination, formation, equality rules
- cartesian product, disjoint union, functions, finite sets
- Introduction to the monomorphic theory
- Explain the cartesian product between two sets.
Wednesday
- Examples of definitions in the monomorphic theory:
- Non-dependent sets: *, +, ->, Bool, Nat, List, Bin
- Dependent sets: Equality, Pi, Sigma, W, U
- Justified the elimination rule for cartesian product,
using some of the semantics.
- Nat, List as an exercise
Thursday
- append as an exercise
- Sigma and show its special case
- Bool as an exercise
- Pi
- Equality
- programming example: the minimal element in a sequence.
Friday
- continuation of the minimal element problem
- introduce the set (Vector n A).
- universes
- document structure
- Some words about work in type theory
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