Abstract |

This chapter gives a survey of *Typelab*, a specification
and verification environment that integrates interactive proof development and
automated proof search. *Typelab* is based on a constructive type
theory, the Calculus of Constructions, which can be understood as a combination of a typed
Lambda calculus and an expressive higher-order
logic. Distinctive features of the type system are dependent function types
(Pi types) for modeling polymorphism and dependent
record types (Sigma types) for encoding specifications and mathematical
theories.

Type theory provides a homogeneous theoretical framework in which the
construction of a function and the construction of a proof can be
considered to be essentially the same activity. There is, however, a practical
difference in that the development of a function requires more insight and
therefore usually has to be performed under human guidance, whereas proof
search can, to a large extent, be automated. Internally, *Typelab* exploits the
homogeneity provided by type theory, while externally offering an interface to
the human user which conceals most of the complexities of type theory.
Interactive construction of proof objects is possible whenever desired;
metavariables serve as placeholders which can be refined incrementally until
the desired object is complete. For procedures which can reasonably be
automated, high-level tactics are available. In this respect, *Typelab* can be
understood as a proof assistant which, in addition to the manipulations of
formulae traditionally performed by theorem provers, permits to carry out
operations on entities such as functions and types.

For an illustration of program development in *Typelab*, the
report UL-TR-98-03 should be consulted,
which holds an extended version of this chapter.

BibTeX Entry |

@Book{Deduction:98, author = {W. Bibel and P. Schmitt}, title = {Automated Deduction --- A Basis for Applications}, publisher = {Kluwer Academic Publishers}, year = {1998} } @InCollection{Strecker:98a, author = {M. Strecker and M. Luther and F. von Henke}, title = {{Interactive and automated proof construction in type theory}}, booktitle = "Automated Deduction --- A Basis for Applications", crossref = {Deduction:98}, publisher = {Kluwer Academic Publishers}, year = 1998, editor = {W. Bibel and P. Schmitt}, volume = {I: Foundations}, chapter = {3: Interactive Theorem Proving} }

Last modified: Sat Nov 11 20:37:38 CET 2006 |