Integration der Logik HOL mit den Programmiersprachen ML und Haskell

点击翻译按钮获取中文摘要

Ziel des Antrags ist die (möglichst) perfekte Integration eines Theorembeweisers und funktionaler Programmiersprachen. Die Grenzen zwischen der funktionalen Kernsprache der Logik HOL und den Programmiersprachen ML und Haskeil soll so weit wie möglich aufgehoben werden. Dazu [ist der Theorembeweiser Isabelle/HOL so zu erweitern, dass man in ihm Funktionen so wie in ML oder Haskell definieren kann (inkl. einer Klasse partieller Funktionen), und dass diese Funktionsdefinitionen als Programme sowohl ex- als auch importiert werden können. Der besondere Schwerpunkt liegt dabei auf der Generierung imperativer Datenstrukturen (Referenzen und Arrays) aus rein funktionalen Isabelle/HOL Spezifikationen mit Hilfe von Monaden (für Haskell) und statischer Analyse (für ML). Eine ähnlich enge Kopplung eines Theorembeweisers an eine moderne funktionale Programmiersprache wie ML oder Haskell, inklusive ihrer imperativen Aspekte, existiert bisher nirgends.