A trustworthy proof checker

DOI10.1023/B:JARS.0000021013.61329.58zbMath1069.68596OpenAlexW1974984092MaRDI QIDQ1826468

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

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-carrying codeproof checker

Mathematics Subject Classification ID

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

Related Items

Verified Software Toolchain, TCB, \texttt{slepice}: towards a verified implementation of type theory in type theory

Uses Software

• Coq
• HOL