Proofs, programs and executable specifications in higher order logic [Elektronische Ressource] / Stefan Berghofer

Stefan Berghofer

Sujets

• Informatik

Informations

• Publié par: technische_universitat_munchen
• Publié le: 01 janvier 2003
• Nombre de lectures: 36
• Langue: Deutsch
• Poids de l'ouvrage: 1 Mo

Extrait

f
f f f
f f f f
f f
f f f
f f f f
f f f
Proofs, Programs and Executable Speci cations
in Higher Order Logic
Stefan Berghofer
Lehrstuhl fur Software&Systems Engineering
Institut fur Informatik
Technische Universitat MunchenLehrstuhl fur Software & Systems Engineering
Institut fur Informatik
Technische Universitat Munch en
Proofs, Programs and Executable Speci cations
in Higher Order Logic
Stefan Berghofer
Vollsant digerAbdruckdervonderFakult atfur InformatikderTechnischenUniversit atMunchen
zur Erlangung des akademischen Grades eines
Doktors der Naturwissenschaften (Dr. rer. nat.)
genehmigten Dissertation.
Vorsitzender: Univ.-Prof. Dr. Dr. h.c. Wilfried Brauer
Pruf er der Dissertation: 1. Univ.-Prof. Tobias Nipkow, Ph.D.
2. Univ.-Prof. Dr. Helmut Schwichtenberg,
Ludwig-Maximilians-Universiatt Mun chen
Die Dissertation wurde am 18. Juni 2003 bei der Technischen Universit at Mun chen eingereicht
und durch die Fakult at fur Informatik am 7. Oktober 2003 angenommen.Kurzfassung
Diese Arbeit paser ntiert mehrere Erweiterungen des generischen Theorembeweisers Isabelle.
Der zentrale Beitrag der Arbeit ist die Erweiterung von Isabelle um einen Kalkul fur primitive
Beweisterme, in dem Beweise als Lambda-Terme repaser ntiert werden. Primitive Beweisterme
erlauben eine unabh angige Veri kation von in Isabelle konstruierten Beweisen durch einen
kleinen und vertrauenswur digen Beweisprufer und bilden eine wichtige Voraussetzung fur den
Austausch von Beweisen mit anderen Systemen.
DerBeweistermkalkul wirdinsbesonderedazuverwendet,umdieBeziehungzwischenBeweisen
und Programmen zu studieren. Hierzu wird ein Mechanismus zur Extraktion von beweisbar
korrektenProgrammenauskonstruktivenBeweisenentwickeltundaufverschiedeneFallstudien
angewandt.
Daruberhinaus stellen wir einen alternativen Ansatz zur Gewinnung von Programmen aus
Spezi kationen vor, der induktive Denitionen direkt als Logikprogramme interpretiert.
iiiAbstract
This thesis presents several extensions to the generic theorem prover Isabelle, a logical frame-
work 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 -terms in the spirit of the Curry-Howard
isomorphism. Primitiveprooftermsallowforanindependentveri cationofproofsconstructed
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 rst develop a generic mechanism for the extraction of prov-
ably correct programs from constructive proofs, then instantiate it for the particular object
logic Isabelle/HOL, and nally apply it to several case studies, ranging from simple textbook
examples to complex applications from the eld of combinatorics or the theory of -calculus.
Moreover, we introduce an alternative approach for obtaining programs from speci cations by
directly interpreting inductive denitions as logic programs.
iii