A guided tour through TYPELAB*
Bericht
Autoren
Luther, Marko
Strecker, Martin
Fakultäten
Fakultät für Ingenieurwissenschaften und InformatikUlmer Schriftenreihe
Ulmer Informatik-Berichte
Zusammenfassung
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.
Erstellung / Fertigstellung
1998
Normierte Schlagwörter
Automatisches Beweisverfahren [GND]Automatic theorem proving; Computer programs [LCSH]
Type theory [LCSH]
DDC-Sachgruppe
DDC 004 / Data processing & computer scienceMetadata
Zur LanganzeigeZitiervorlage
Luther, Marko; Strecker, Martin (2013): A guided tour through TYPELAB*. Open Access Repositorium der Universität Ulm. http://dx.doi.org/10.18725/OPARU-2491