Turning Inductive into Equational Specifications

DOI10.1007/978-3-642-03359-9_11MaRDI QIDQ3183524zbMATH OpenOpenAlexFDO

Authors Stefan Berghofer, Lukas Bulwahn, Florian Haftmann

Publication date 20 October 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-03359-9_11

Mathematics Subject Classification ID

Logic programming (68N17) Specification and verification (program logics, model checking, etc.) (68Q60) Functional programming and lambda calculus (68N18)

Recommendations

• Inductive proofs by specification transformations
• Code generation via higher-order rewrite systems
• Producing certified functional code from inductive specifications
• Deductive and inductive synthesis of equational programs
• scientific article; zbMATH DE number 4074541

Cites work

• scientific article; zbMATH DE number 2085164 (Why is no real title available?)
• A Mechanized Model of the Theory of Objects
• Extracting Purely Functional Contents from Logical Inductive Types
• The execution algorithm of mercury, an efficient purely declarative logic programming language
• Java: Embedding a programming language in a theorem prover

Cited in

(7)

• First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification
• Teaching semantics with a proof assistant: no more LSD trip proofs
• From LCF to Isabelle/HOL
• A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL
• Animating the formalised semantics of a Java-like language
• Code generation via higher-order rewrite systems
• Foundational property-based testing

Describes a project that uses

Uses Software

• Mercury
• OCaml
• Haskell
• Isabelle/HOL
• Isabelle

This page was built for publication: Turning Inductive into Equational Specifications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3183524)