Foundational Proof Checkers with Small Witnesses

Dinghao Wu, Andrew W. Appel, Aaron Stump

Research output: Chapter in Book/Report/Conference proceedingConference contribution

26 Scopus citations

Abstract

Proof checkers for proof-carrying code (and similar systems) can suffer from two problems: huge proof witnesses and untrustworthy proof rules. No previous design has addressed both of these problems simultaneously. We show the theory, design, and implementation of a proof-checker that permits small proof witnesses and machine-checkable proofs of the soundness of the system.

Original languageEnglish (US)
Title of host publicationProceedings of the Fifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming, (PPDP 03)
PublisherAssociation for Computing Machinery
Pages264-274
Number of pages11
ISBN (Print)1581137052, 9781581137057
DOIs
StatePublished - Jan 1 2003
EventFifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming - Uppsala, Sweden
Duration: Aug 27 2003Aug 29 2003

Publication series

NameProceedings of the ACM SIGPLAN Conference on Principles and Practice of Declarative Programming
Volume5

Other

OtherFifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming
CountrySweden
CityUppsala
Period8/27/038/29/03

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Proof Checker
  • Proof-Carrying Code

Cite this

Wu, D., Appel, A. W., & Stump, A. (2003). Foundational Proof Checkers with Small Witnesses. In Proceedings of the Fifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming, (PPDP 03) (pp. 264-274). (Proceedings of the ACM SIGPLAN Conference on Principles and Practice of Declarative Programming; Vol. 5). Association for Computing Machinery. https://doi.org/10.1145/888251.888276