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.     «

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...     »

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.     «

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....     »