Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation
- 1 January 2013
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
Abstract
Proof-by-reflection is a well-established technique that employs decision procedures to reduce the size of proof-terms. Currently, decision procedures can be written either in Type Theory—in a purely functional way that also ensures termination— or in an effectful programming language, where they are used as oracles for the certified checker. The first option offers strong correctness guarantees, while the second one permits more efficient implementations. We propose a novel technique for proof-by-reflection that marries, in Type Theory, an effectful language with (partial) proofs of correctness. The key to our approach is to use simulable monads, where a monad is simulable if, for all terminating reduction sequences in its equivalent effectful computational model, there exists a witness from which the same reduction may be simulated a posteriori by the monad. We encode several examples using simulable monads and demonstrate the advantages of the technique over previous approaches.Keywords
This publication has 13 references indexed in Scilit:
- Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful ComputationLecture Notes in Computer Science, 2013
- How to make ad hoc proof automation less ad hocPublished by Association for Computing Machinery (ACM) ,2011
- Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem ProvingLecture Notes in Computer Science, 2011
- Certifying compilers using higher-order theorem provers as certificate checkersFormal Methods in System Design, 2010
- Extending Coq with Imperative Features and Its Application to SAT VerificationLecture Notes in Computer Science, 2010
- Extraction in Coq: An OverviewPublished by Springer Science and Business Media LLC ,2008
- Computation by ProphecyLecture Notes in Computer Science, 2007
- Term Rewriting and All ThatPublished by Cambridge University Press (CUP) ,1998
- Using reflection to build efficient and certified decision proceduresPublished by Springer Science and Business Media LLC ,1997
- Edinburgh LCFLecture Notes in Computer Science, 1979