Logo des Repositoriums
 
Textdokument

Programmierung, Spezifikation und Interaktives Beweisen

Lade...
Vorschaubild

Volltext URI

Dokumententyp

Zusatzinformation

Datum

2003

Zeitschriftentitel

ISSN der Zeitschrift

Bandtitel

Verlag

Gesellschaft für Informatik

Zusammenfassung

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.

Beschreibung

Stehr, Mark-Oliver (2003): Programmierung, Spezifikation und Interaktives Beweisen. Ausgezeichnete Informatikdissertationen 2002. Bonn: Gesellschaft für Informatik. PISSN: 1617-5468. ISBN: 978-3-88579-407-1. pp. 185-199

Schlagwörter

Zitierform

DOI

Tags