Transforming Programs into Recursive Functions

DOI10.1016/j.entcs.2009.05.052zbMath1347.68304OpenAlexW2079552794MaRDI QIDQ5179363

Michael J. C. Gordon, Magnus O. Myreen

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

theorem provingprogram verification

Mathematics Subject Classification ID

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

Related Items (3)

Loop verification with invariants and contracts ⋮ Equivalence checking of two functional programs using inductive theorem provers ⋮ Function extraction

Uses Software

• ACL2
• HOL

Cites Work

• Partial functions in ACL2
• A Brief Overview of HOL4
• Verification of non-functional programs using interpretations in type theory
• Verification Condition Generation Via Theorem Proving
• An axiomatic basis for computer programming
• Correct Hardware Design and Verification Methods

This page was built for publication: Transforming Programs into Recursive Functions