Certifying compilers using higher-order theorem provers as certificate checkers

DOI10.1007/s10703-010-0108-7zbMath1211.68074OpenAlexW2052581162WikidataQ122870988 ScholiaQ122870988MaRDI QIDQ633302

Benjamin Grégoire, Jan Olaf Blech

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

zbMATH Keywords

theorem provingIsabelle/HOLCoqtranslation validationcompiler correctness

Mathematics Subject Classification ID

Uses Software

• ACL2
• Coq
• Isabelle/HOL
• TVOC
• Piton

Cites Work

• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• Formal verification of translation validators
• A Computational Approach to Pocklington Certificates in Type Theory
• Automated soundness proofs for dataflow analyses and transformations via local rules
• Formal certification of a compiler back-end or
• Theorem Proving in Higher Order Logics
• Computer Aided Verification

This page was built for publication: Certifying compilers using higher-order theorem provers as certificate checkers