Reasoning about CBV functional programs in Isabelle/HOL

DOI10.1007/978-3-540-30142-4_15MaRDI QIDQ5464647zbMATH OpenOpenAlexFDO

Authors John Longley, Randy Pollack

Publication date 18 August 2005

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

Full work available at URL https://doi.org/10.1007/b100400

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Imperative Functional Programming with Isabelle/HOL
• A Hoare Logic for Call-by-Value Functional Programs
• scientific article; zbMATH DE number 2110621
• Concrete semantics. With Isabelle/HOL
• A verification environment for sequential imperative programs in Isabelle/HOL

Cited in

(5)

• Reasoning about resources in the embedded systems language Hume
• A Hoare Logic for Call-by-Value Functional Programs
• Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL
• scientific article; zbMATH DE number 7649970 (Why is no real title available?)
• A proof tool for reasoning about functional programs

Describes a project that uses

Uses Software

• Isabelle
• ML
• Isabelle/HOL

This page was built for publication: Reasoning about CBV functional programs in Isabelle/HOL

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