Anzeige
Erschienen in:
2009 | OriginalPaper | Buchkapitel
Turning Inductive into Equational Specifications
verfasst von : Stefan Berghofer, Lukas Bulwahn, Florian Haftmann
Erschienen in: Theorem Proving in Higher Order Logics
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. 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.