Berghofer, Stefan

Proofs, Programs and Executable Specifications in Higher Order Logic

Beweise, Programme und ausführbare Spezifikationen in höherstufiger Logik

Thesis

 Filetyp: PDF (.pdf)
Size: 1180 Kb

Schlüsselwörter:

proof terms, Curry-Howard isomorphism, constructive logic, program extraction, executable specifications

Beweisterme, Curry-Howard Isomorphismus, konstruktive Logik, Programmextraktion, ausführbare Spezifikationen

TUB Systematik
DAT 540d; DAT 706d
Schlagwortnormdatei
Logische Programmierung / Softwarespezifikation; Automatisches Beweisverfahren / Logische Programmierung / Konstruktive Logik
Sachgruppe der DNB
28 Informatik, Datenverarbeitung
ACM Computing Classification System
I.2.2, I.2.3, F.4.1

Dissertation eingereicht bei: Technische Universität München , Fakultät für Informatik, 2003-06-18
Tag der mündlichen Prüfung: 2003-10-20

Abstract in English

This thesis presents several extensions to the generic theorem prover Isabelle, a logical framework based on higher order logic.
The central contribution of this thesis is the extension of Isabelle with a calculus of primitive proof terms, in which proofs are represented using lambda-terms in the spirit of the Curry-Howard isomorphism. Primitive proof terms allow for an independent verification of proofs constructed in Isabelle by a small and reliable proof checker, and are an important prerequisite for the application of proof transformation and analysis techniques, as well as the exchange of proofs with other systems.
In particular, the proof term calculus is used to study the relationship between proofs and programs. For this purpose, we first develop a generic mechanism for the extraction of provably correct programs from constructive proofs, then instantiate it for the particular object logic Isabelle/HOL, and finally apply it to several case studies, ranging from simple textbook examples to complex applications from the field of combinatorics or the theory of lambda-calculus.
Moreover, we introduce an alternative approach for obtaining programs from specifications by directly interpreting inductive definitions as logic programs.

Abstract in Deutsch

Diese Arbeit präsentiert mehrere Erweiterungen des generischen Theorembeweisers Isabelle. Der zentrale Beitrag der Arbeit ist die Erweiterung von Isabelle um einen Kalkül für primitive Beweisterme, in dem Beweise als Lambda-Terme repräsentiert werden. Primitive Beweisterme erlauben eine unabhängige Verifikation von in Isabelle konstruierten Beweisen durch einen kleinen und vertrauenswürdigen Beweisprüfer und bilden eine wichtige Voraussetzung für den Austausch von Beweisen mit anderen Systemen.
Der Beweistermkalkül wird insbesondere dazu verwendet, um die Beziehung zwischen Beweisen und Programmen zu studieren. Hierzu wird ein Mechanismus zur Extraktion von beweisbar korrekten Programmen aus konstruktiven Beweisen entwickelt und auf verschiedene Fallstudien angewandt.
Darüberhinaus stellen wir einen alternativen Ansatz zur Gewinnung von Programmen aus Spezifikationen vor, der induktive Definitionen direkt als Logikprogramme interpretiert.

Betreuer Nipkow, T.; Univ.-Prof. Ph.D.
Gutachter Nipkow, T.; Univ.-Prof. Ph.D.
Gutachter Schwichtenberg, H.; Univ.-Prof. Dr., Ludwig-Maximilians-Universität München
Upload: 2003-10-28
URL of Theses: http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2003/berghofer.pdf

Technische Universität München, Universitätsbibliothek
Arcisstr. 21, D-80333 München
Unversehrtheit der Publikation Unversehrtheit der Publikation