Imperative Functional Programming with Isabelle/HOL

We introduce a lightweight approach for reasoning about programs involving imperative data structures using the proof assistant Isabelle/HOL. It is based on shallow embedding of programs, a polymorphic heap model using enumeration encodings and type classes, and a state-exception monad similar to known counterparts from Haskell. Existing proof automation tools are easily adapted to provide a verification environment. The framework immediately allows for correct code generation to ML and Haskell. Two case studies demonstrate our approach: An array-based checker for resolution proofs, and a more efficient bytecode verifier.

• Type: Conference
• Year: 2008
• Where: TPHOL
• Authors: Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkök, John Matthews
• Keywords: Artificial Intelligence, Imperative Data Structures, Polymorphic Heap Model, Proof Assistant Isabelle/hol, TPHOL 2008