Foundational Proof Checkers with Small Witnesses

Dinghao Wu, Andrew W. Appel, Aaron Stump

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

25 Citations (Scopus)

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)
Pages264-274
Number of pages11
StatePublished - Dec 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

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).
Wu, Dinghao ; Appel, Andrew W. ; Stump, Aaron. / Foundational Proof Checkers with Small Witnesses. Proceedings of the Fifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming, (PPDP 03). 2003. pp. 264-274 (Proceedings of the ACM SIGPLAN Conference on Principles and Practice of Declarative Programming).
@inproceedings{055575cd2a284a738d492153f13700b4,
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.",
author = "Dinghao Wu and Appel, {Andrew W.} and Aaron Stump",
year = "2003",
month = "12",
day = "1",
language = "English (US)",
isbn = "1581137052",
series = "Proceedings of the ACM SIGPLAN Conference on Principles and Practice of Declarative Programming",
pages = "264--274",
booktitle = "Proceedings of the Fifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming, (PPDP 03)",

}

Wu, D, Appel, AW & 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). Proceedings of the ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, vol. 5, pp. 264-274, Fifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming, Uppsala, Sweden, 8/27/03.

Foundational Proof Checkers with Small Witnesses. / Wu, Dinghao; Appel, Andrew W.; Stump, Aaron.

Proceedings of the Fifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming, (PPDP 03). 2003. p. 264-274 (Proceedings of the ACM SIGPLAN Conference on Principles and Practice of Declarative Programming; Vol. 5).

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

TY - GEN

T1 - Foundational Proof Checkers with Small Witnesses

AU - Wu, Dinghao

AU - Appel, Andrew W.

AU - Stump, Aaron

PY - 2003/12/1

Y1 - 2003/12/1

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

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)

ER -

Wu D, Appel AW, Stump A. Foundational Proof Checkers with Small Witnesses. In Proceedings of the Fifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming, (PPDP 03). 2003. p. 264-274. (Proceedings of the ACM SIGPLAN Conference on Principles and Practice of Declarative Programming).