A trustworthy proof checker

DOI10.1023/B:JARS.0000021013.61329.58MaRDI QIDQ1826468zbMATH OpenOpenAlexFDO

Authors Andrew W. Appel, Neophytos Michael, Aaron Stump, Roberto Virga

Publication date 6 August 2004

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/b:jars.0000021013.61329.58

zbMATH Keywords

proof checkerproof-carrying code

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 2090287
• scientific article; zbMATH DE number 2110618
• scientific article; zbMATH DE number 1962754
• scientific article; zbMATH DE number 1330435
• Oracle-based checking of untrusted software

Cited in

(11)

• Trusted computing with addition machines. II
• Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)
• \texttt{slepice}: towards a verified implementation of type theory in type theory
• TCB
• Verified software toolchain (invited talk)
• The Proof Certifier Checkers
• scientific article; zbMATH DE number 1956568 (Why is no real title available?)
• scientific article; zbMATH DE number 2090287 (Why is no real title available?)
• Oracle-based checking of untrusted software
• Logic for Programming, Artificial Intelligence, and Reasoning
• Proof checking and logic programming

Describes a project that uses

Uses Software

• HOL
• Coq

This page was built for publication: A trustworthy proof checker

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1826468)