Programmierung, Spezifikation und Interaktives Beweisen

Abstract

Diese Dissertation mit dem englischen Titel “Programming, Specification, and Interactive Theorem Proving – Towards a Unified Language based on Equational Logic, Rewriting Logic, and Type Theory” bescha ̈ftigt sich mit dem Problem der Inflation von Formalismen in der Informatik im Kontext eines Spektrums formaler Methoden, das von Ausführung, über Analyse, bis zur formalen Verifikation reicht. Durch ihre Repräsentation in semantischen und logischen Rahmenwerken (semantic and logical frameworks), wie der Gleichungslogik (equational logic), der Termersetzungslogik (rewriting logic), oder der Typtheorie, wird ein Beitrag zum besseren Verständnis der Formalismen sowie ihrer Beziehungen untereinander geliefert. Konkret behandeln wir verschiedene Klassen von Petrinetzen, die UNITY-Temporallogik, das -Kalkül, Abadi und Cardellis -Kalkül, Milners -Kalkül, sowie verschiedene logische Typtheorien. Gleichzeitig studieren wir interessante Verallgemeinerungen der repräsentierten Formalismen und weisen die Praxistauglichkeit des formalen Rahmens durch eine Reihe von Anwendungen nach. In einem weiteren Vereinheitlichungsschritt wird ein neues Rahmenwerk, das Kalkül der offenen Konstruktionen (open calculus of constructions), eingeführt, das die Ideen der Gleichungslogik, der Termersetzungslogik, und der Typtheorie in einer relativ einfachen Sprache zusammenführt. Der Einsatz als Programmier- und Spezifikationssprache, sowie als Formalismus zum interaktiven Beweisen, wird anhand eines Prototyps und zahlreicher Beispiele demonstriert.