Imperative Functional Programming with Isabelle/HOL
Lukas Bulwahn, Alexandar Krauss, Florian Haftmann,
Levent Erkok, John Matthews
Appears in TPHOLs '08

---

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.