A guided tour through TYPELAB*

Abstract

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.