### 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) |

Publisher | Association for Computing Machinery |

Pages | 264-274 |

Number of pages | 11 |

ISBN (Print) | 1581137052, 9781581137057 |

DOIs | |

State | Published - Jan 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

### Keywords

- Proof Checker
- Proof-Carrying Code

## 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). Association for Computing Machinery. https://doi.org/10.1145/888251.888276