TY - GEN
T1 - Foundational Proof Checkers with Small Witnesses
AU - Wu, Dinghao
AU - Appel, Andrew W.
AU - Stump, Aaron
PY - 2003
Y1 - 2003
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=1242287817&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=1242287817&partnerID=8YFLogxK
U2 - 10.1145/888251.888276
DO - 10.1145/888251.888276
M3 - Conference contribution
AN - SCOPUS:1242287817
SN - 1581137052
SN - 9781581137057
T3 - Proceedings of the ACM SIGPLAN Conference on Principles and Practice of Declarative Programming
SP - 264
EP - 274
BT - Proceedings of the Fifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming, (PPDP 03)
PB - Association for Computing Machinery
T2 - Fifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming
Y2 - 27 August 2003 through 29 August 2003
ER -