Turning Inductive into Equational Specifications
| Autor: | Lukas Bulwahn, Florian Haftmann, Stefan Berghofer |
|---|---|
| Rok vydání: | 2009 |
| Předmět: |
Theoretical computer science
Computer science Programming language Proof assistant computer.software_genre Automated theorem proving TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Formal specification Haskell Code generation computer Scope (computer science) Logic programming computer.programming_language Data-flow analysis |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783642033582 TPHOLs |
| DOI: | 10.1007/978-3-642-03359-9_11 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|