@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",

note = "Copyright: Copyright 2020 Elsevier B.V., All rights reserved.; Fifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming ; Conference date: 27-08-2003 Through 29-08-2003",

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)",

}