| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 9656074 | Electronic Notes in Theoretical Computer Science | 2005 | 19 Pages |
Abstract
We have developed denotational proof languages (DPLs) as a uniform platform for certified computation. DPLs integrate computation and deduction seamlessly, offer strong soundness guarantees, and provide versatile mechanisms for constructing proofs and proof-search methods. We have used DPLs to implement numerous well-known algorithms as certifiers, ranging from sorting algorithms to compiler optimizations, the Hindley-Milner W algorithm, Prolog engines, and more.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Konstantine Arkoudas, Martin Rinard,