# 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