• English
    • Deutsch
Dokumentanzeige 
  •   OPARU Startseite
  • Fakultät für Ingenieurwissenschaften, Informatik und Psychologie
  • Publikationen
  • Dokumentanzeige
  •   OPARU Startseite
  • Fakultät für Ingenieurwissenschaften, Informatik und Psychologie
  • Publikationen
  • Dokumentanzeige
  • Deutsch 
    • English
    • Deutsch
  • Einloggen
JavaScript is disabled for your browser. Some features of this site may not work without it.

A guided tour through TYPELAB*

Thumbnail
Download
vts_8520_12569.pdf (173.4Kb)
36 S.
 
Veröffentlichung
2013-06-06
DOI
10.18725/OPARU-2491

Bericht

Autoren
Luther, Marko
Strecker, Martin
Fakultäten
Fakultät für Ingenieurwissenschaften und Informatik
Ulmer Schriftenreihe
Ulmer Informatik-Berichte
Lizenz
Standard
https://oparu.uni-ulm.de/xmlui/license_v3
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 science

Metadata
Zur Langanzeige

Zitiervorlage

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

Weitere Zitierstile



Informationen zu OPARU | Kontakt | Feedback
Impressum | Datenschutzerklärung
 

 

Erweiterte Suche

Stöbern

Gesamter BestandBereiche & SammlungenFakultätenInstitutionenPersonenRessourcentypenUlmer Reihen & ZeitschriftenDDC-SachgruppenFörderinformationenAusgewählte SammlungFakultätenInstitutionenPersonenRessourcentypenUlmer Reihen & ZeitschriftenDDC-SachgruppenFörderinformationen

Mein Benutzerkonto

EinloggenRegistrieren

Statistik

Benutzungsstatistik

Informationen zu OPARU | Kontakt | Feedback
Impressum | Datenschutzerklärung