Refinement calculus for logic programming in Isabelle/HOL

DOI10.1007/3-540-44755-5_18MaRDI QIDQ4790664zbMATH OpenFDO

Authors David Hemer, Ian Hayes, Paul Strooper

Publication date 4 February 2003

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2152/21520249

Mathematics Subject Classification ID

Logic programming (68N17)

Recommendations

• A refinement calculus for logic programs
• A tool for logic program refinement (extended abstract)
• Intuitionistic Refinement Calculus
• Refinement of Higher-Order Logic Programs
• Expression refinement in higher order logic

Cited in

(12)

• The least conjunctive refinement and promotion in the refinement calculus
• Mechanizing some advanced refinement concepts
• General parameterised refinement and recursion for the M-net calculus
• From proposition to program. Embedding the refinement calculus in Coq
• Refinement trees: calculi, tools, and applications
• Intuitionistic Refinement Calculus
• A tool for logic program refinement (extended abstract)
• An embedding of Ruby in Isabelle
• scientific article; zbMATH DE number 2110621 (Why is no real title available?)
• Representing WP semantics in Isabelle/ZF
• A theoretical basis for stepwise refinement and the programming calculus
• A sequent calculus for first-order logic formalized in Isabelle/HOL

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL
• Isabelle/ZF

This page was built for publication: Refinement calculus for logic programming in Isabelle/HOL

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