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. © 2013 Springer-Verlag.
CITATION STYLE
Claret, G., Del Carmen González Huesca, L., Régis-Gianas, Y., & Ziliani, B. (2013). Lightweight proof by reflection using a posteriori simulation of effectful computation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7998 LNCS, pp. 67–83). https://doi.org/10.1007/978-3-642-39634-2_8
Mendeley helps you to discover research relevant for your work.