Advertisement
Published in:
2009 | OriginalPaper | Chapter
Turning Inductive into Equational Specifications
Authors : Stefan Berghofer, Lukas Bulwahn, Florian Haftmann
Published in: Theorem Proving in Higher Order Logics
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Inductively defined predicates are frequently used in formal specifications. Using the theorem prover
Isabelle
, we describe an approach to turn a class of systems of inductively defined 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.