Certifying compilers using higher-order theorem provers as certificate checkers
From MaRDI portal
Publication:633302
DOI10.1007/S10703-010-0108-7zbMATH Open1211.68074OpenAlexW2052581162WikidataQ122870988 ScholiaQ122870988MaRDI QIDQ633302FDOQ633302
Authors: Jan Olaf Blech, Benjamin Grégoire 
Publication date: 31 March 2011
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10703-010-0108-7
Recommendations
Cites Work
- Computer Aided Verification
- Isabelle/HOL. A proof assistant for higher-order logic
- A Computational Approach to Pocklington Certificates in Type Theory
- Theorem Proving in Higher Order Logics
- Title not available (Why is that?)
- Formal verification of translation validators
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- Title not available (Why is that?)
- Automated soundness proofs for dataflow analyses and transformations via local rules
Cited In (7)
Uses Software
This page was built for publication: Certifying compilers using higher-order theorem provers as certificate checkers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q633302)
