Transforming programs into recursive functions

DOI10.1016/J.ENTCS.2009.05.052MaRDI QIDQ5179363zbMATH OpenOpenAlexFDO

Authors Magnus O. Myreen, Michael J. C. Gordon

Publication date 19 March 2015

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2009.05.052

zbMATH Keywords

program verificationtheorem proving

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1615264
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• scientific article; zbMATH DE number 785053
• scientific article; zbMATH DE number 1555192
• Automatically Introducing Tail Recursion in CakeML

Cites work

• A Brief Overview of HOL4
• An axiomatic basis for computer programming
• Inductive assertions and operational semantics
• Partial functions in ACL2
• Verification Condition Generation Via Theorem Proving
• Verification of non-functional programs using interpretations in type theory

Cited in

(6)

• Loop verification with invariants and contracts
• Equivalence checking of two functional programs using inductive theorem provers
• Function extraction
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• Invariant relations for affine loops
• Deaccumulation techniques for improving provability

Describes a project that uses

Uses Software

• ACL2
• HOL

This page was built for publication: Transforming programs into recursive functions

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