Turning Inductive into Equational Specifications

DOI10.1007/978-3-642-03359-9_11zbMath1252.68249OpenAlexW1486298687MaRDI QIDQ3183524

Lukas Bulwahn, Stefan Berghofer, 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

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

Related Items (6)

Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs ⋮ Foundational Property-Based Testing ⋮ First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification ⋮ A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL ⋮ From LCF to Isabelle/HOL ⋮ Animating the Formalised Semantics of a Java-Like Language

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Extracting Purely Functional Contents from Logical Inductive Types
• The execution algorithm of mercury, an efficient purely declarative logic programming language
• A Mechanized Model of the Theory of Objects

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