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 -