User: Guest  Login
Original title:
Proofs, Programs and Executable Specifications in Higher Order Logic 
Translated title:
Beweise, Programme und ausführbare Spezifikationen in höherstufiger Logik 
Year:
2003 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Nipkow, Tobias (Prof. Ph.D.) 
Referee:
Nipkow, Tobias (Prof. Ph.D.); Schwichtenberg, Helmut (Prof. Dr.) 
Format:
Text 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik 
Keywords:
proof terms; Curry-Howard isomorphism; constructive logic; program extraction; executable specifications 
Translated keywords:
Beweisterme; Curry-Howard Isomorphismus; konstruktive Logik; Programmextraktion; ausführbare Spezifikationen 
Controlled terms:
Logische Programmierung; Softwarespezifikation; Automatisches Beweisverfahren; Konstruktive Logik 
TUM classification:
DAT 540d; DAT 706d 
Abstract:
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 prerequi...    »
 
Translated abstract:
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....    »
 
Publication :
Universitätsbibliothek der TU München 
Oral examination:
20.10.2003 
File size:
1208305 bytes 
Pages:
175 
Last change:
04.07.2007