Sciweavers

Share
TPHOL
2008
IEEE

Imperative Functional Programming with Isabelle/HOL

8 years 9 months ago
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.
Lukas Bulwahn, Alexander Krauss, Florian Haftmann,
Added 01 Jun 2010
Updated 01 Jun 2010
Type Conference
Year 2008
Where TPHOL
Authors Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkök, John Matthews
Comments (0)
books