Programs from Proofs - A PCC Alternative
No abstract available.
Related papers
- An indexed model of recursive types for foundational proof-carrying code TOPLAS 2001
- Oracle-based checking of untrusted software POPL 2001
- Programs from Proofs: A Framework for the Safe Execution of Untrusted Software TOPLAS 2017
- A certifying compiler for Java PLDI 2000
- Proof-Carrying Code POPL 1997
- Building Certified Libraries for PCC: Dynamic Storage Allocation ESOP 2003
- Certified assembly programming with embedded code pointers POPL 2006
- Modular verification of assembly code with stack-based control abstractions PLDI 2006