Stefan Berghofer, Lukas Bulwahn, Florian Haftmann (itestra GmbH)
Turning Inductive into Equational Specifications
Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009
Abstract
Inductively de ned predicates are frequently used in formal speci cations. Using the theorem prover Isabelle, we describe an approach to turn a class of systems of inductively de ned predicates into a system of equations using data flow analysis; the translation is carried out inside the logic and resulting equations can be turned into functional program code in SML, OCaml or Haskell using the existing code generator of Isabelle. Thus we extend the scope of code generation in Isabelle from functional to functional-logic programs while leaving the trusted foundations of code generation itself intact.
