Interactive and automated proof construction in type theory

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}
}