@inproceedings{fcf808d77d7948248d601bde2e872246,
title = "Foundational Proof Checkers with Small Witnesses",
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.",
keywords = "Proof Checker, Proof-Carrying Code",
author = "Dinghao Wu and Appel, {Andrew W.} and Aaron Stump",
year = "2003",
doi = "10.1145/888251.888276",
language = "English (US)",
isbn = "1581137052",
series = "Proceedings of the ACM SIGPLAN Conference on Principles and Practice of Declarative Programming",
publisher = "Association for Computing Machinery",
pages = "264--274",
booktitle = "Proceedings of the Fifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming, (PPDP 03)",
note = "Fifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming ; Conference date: 27-08-2003 Through 29-08-2003",
}