Abstract |

This dissertation is concerned with interactive proof construction and automated proof search in type theories, in particular the Calculus of Constructions and its subsystems.

Type theories can be conceived as expressive logics which combine a functional programming language, strong typing and a higher-order logic. They are therefore a suitable formalism for specification and verification systems. However, due to their expressiveness, it is difficult to provide appropriate deductive support for type theories. This dissertation first examines general methods for proof construction in type theories and then explores how these methods can be refined to yield proof search procedures for specialized fragments of the language.

Proof development in type theories usually requires the
construction of a term having a given type in a given context. For the term to
be constructed, a *metavariable* is introduced which is successively
instantiated in the course of the proof. A naive use of metavariables leads to
problems, such as non-commutativity of reduction and instantiation and the
generation of ill-typed terms during reduction. For solving these problems, a
calculus with *explicit substitutions* is introduced, and it is shown
that this calculus preserves properties such as strong normalization and
decidability of typing.

In order to obtain a calculus appropriate for proof search, the usual natural
deduction presentation of type theories is replaced by a *sequent style
presentation*. It is shown that the calculus thus obtained is correct with
respect to the original calculus. Completeness (proved with a cut-elimination
argument) is shown for all predicative fragments of the lambda cube.

The dissertation concludes with a discussion of some techniques that make
proof search practically applicable, such as unification and pruning of the
proof search space by exploiting impermutabilities of the sequent calculus.

Online Copy |

PDF File, final version (1.5 MB)

BibTeX Entry |

@PhdThesis{Strecker:PhD, author = {Martin Strecker}, title = {Construction and Deduction in Type Theories}, school = {Universit{\"a}t Ulm}, year = 1999 }

Last modified: Sat Nov 11 20:33:56 CET 2006 |