### 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 language | English (US) |
---|---|

Title of host publication | Proceedings of the Fifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming, (PPDP 03) |

Pages | 264-274 |

Number of pages | 11 |

State | Published - Dec 1 2003 |

Event | Fifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming - Uppsala, Sweden Duration: Aug 27 2003 → Aug 29 2003 |

### Publication series

Name | Proceedings of the ACM SIGPLAN Conference on Principles and Practice of Declarative Programming |
---|---|

Volume | 5 |

### Other

Other | Fifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming |
---|---|

Country | Sweden |

City | Uppsala |

Period | 8/27/03 → 8/29/03 |

### All Science Journal Classification (ASJC) codes

- Software

### Cite this

*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).

}

*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.

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 -