Function extraction
From MaRDI portal
Publication:436372
DOI10.1016/j.scico.2010.10.001zbMath1243.68139OpenAlexW2912721414MaRDI QIDQ436372
Magnus O. Myreen, Michael J. C. Gordon
Publication date: 20 July 2012
Published in: Science of Computer Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.scico.2010.10.001
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Efficient weakest preconditions
- Partial functions in ACL2
- A Formalisation of Smallfoot in HOL
- Types, bytes, and separation logic
- Using XCAP to Certify Realistic Systems Code: Machine Context Management
- A Brief Overview of HOL4
- Proving Theorems about LISP Functions
- Automated proofs of object code for a widely used microprocessor
- Stack-based typed assembly language
- Verification of non-functional programs using interpretations in type theory
- Avoiding exponential explosion
- Transforming Programs into Recursive Functions
- Verified just-in-time compiler on x86
- Computer Science Logic
- Formal certification of a compiler back-end or
- Certified assembly programming with embedded code pointers
- Verification Condition Generation Via Theorem Proving
- Theorem Proving in Higher Order Logics
- An axiomatic basis for computer programming
This page was built for publication: Function extraction
