Conference proceeding
Foundational proof checkers with small witnesses
Proceedings of the 5th ACM SIGPLAN international conference on principles and practice of declaritive programming, Vol.5, pp.264-274
PPDP '03
08/27/2003
DOI: 10.1145/888251.888276
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.
Details
- Title: Subtitle
- Foundational proof checkers with small witnesses
- Creators
- Dinghao Wu - Princeton UniversityAndrew Appel - Princeton UniversityAaron Stump - Washington University in St. Louis
- Resource Type
- Conference proceeding
- Publication Details
- Proceedings of the 5th ACM SIGPLAN international conference on principles and practice of declaritive programming, Vol.5, pp.264-274
- Series
- PPDP '03
- DOI
- 10.1145/888251.888276
- Publisher
- ACM
- Language
- English
- Date published
- 08/27/2003
- Academic Unit
- Computer Science
- Record Identifier
- 9984259435902771
Metrics
6 Record Views