A guided tour through Typelab

Marko Luther, Martin Strecker

Published as Technical Report Nr. 98-03
Ulmer Informatik Berichte
January 1998


This report 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 for modeling polymorphism and dependent record types for encoding specifications and mathematical theories. After presenting an extended example which demonstrates how program development by stepwise refinement of specifications can be carried out, the theory underlying the prover component of Typelab is described in detail. A calculus with metavariables and explicit substitutions is introduced, and the meta-theoretic properties of this calculus are analyzed. Furthermore, it is shown that this calculus provides an adequate foundation for automated proof search in fragments of the logic.

This technical report is an extended version of the book chapter Interactive and automated proof construction in type theory.

 Online Copy

Available as Postscript (417 KB)

 BibTeX Entry

  author = 	 {Marko Luther and Martin Strecker},
  title = 	 {A guided tour through {\sc Typelab}},
  institution =  {Universit{\"a}t Ulm},
  year = 	 1998,
  number =	 {98-03},
  month =	 {January}

Last modified: Sat Nov 11 20:33:35 CET 2006