Function extraction
From MaRDI portal
Publication:436372
DOI10.1016/J.SCICO.2010.10.001zbMATH Open1243.68139OpenAlexW2912721414MaRDI QIDQ436372FDOQ436372
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
Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A Brief Overview of HOL4
- An axiomatic basis for computer programming
- Partial functions in ACL2
- Verified just-in-time compiler on x86
- Certified assembly programming with embedded code pointers
- Proving Theorems about LISP Functions
- Stack-based typed assembly language
- Efficient weakest preconditions
- A Formalisation of Smallfoot in HOL
- Types, bytes, and separation logic
- Using XCAP to Certify Realistic Systems Code: Machine Context Management
- Automated proofs of object code for a widely used microprocessor
- Verification of non-functional programs using interpretations in type theory
- Avoiding exponential explosion
- Transforming Programs into Recursive Functions
- Computer Science Logic
- Formal certification of a compiler back-end or
- Verification Condition Generation Via Theorem Proving
- Theorem Proving in Higher Order Logics
Cited In (3)
Uses Software
Recommendations
This page was built for publication: Function extraction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q436372)
