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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Armand, M., Grégoire, B., Spiwack, A., Théry, L.: Extending Coq with Imperative Features and its Application to SAT Verification. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 83–98. Springer, Heidelberg (2010)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge Univ. Press (1998)
Blech, J.O., Grégoire, B.: Certifying compilers using higher-order theorem provers as certificate checkers. FMSD (2011)
Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol. 1281, pp. 515–529. Springer, Heidelberg (1997)
Bove, A., Capretta, V.: Computation by prophecy. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 70–83. Springer, Heidelberg (2007)
Claret, G., González Huesca, L., Régis-Gianas, Y., Ziliani, B.: Lightweight proof by reflection using a posteriori simulation of effectful computation. Technical report (2013), http://cybele.gforge.inria.fr/download/cybele_technical_report.pdf
Corbineau, P.: Autour de la clôture de congruence avec coq. Master’s thesis, ENS (2001) (in French)
Gonthier, G., Ziliani, B., Nanevski, A., Dreyer, D.: How to make ad hoc proof automation less ad hoc. In: ICFP (2011)
Gordon, M.J., Wadsworth, C.P., Milner, R.: Edinburgh LCF. LNCS, vol. 78. Springer, Heidelberg (1979)
Grégoire, B., Pottier, L., Théry, L.: Proof certificates for algebra and their application to automatic geometry theorem proving. In: Sturm, T., Zengler, C. (eds.) ADG 2008. LNCS, vol. 6301, pp. 42–59. Springer, Heidelberg (2011)
Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical report, SRI Cambridge (1995)
James, D.W.H., Hinze, R.: A Reflection-based Proof Tactic for Lattices in Coq. In: TFP (2009)
Letouzey, P.: Extraction in Coq: An Overview. In: Beckmann, A., Dimitracopoulos, C., Löwe, B. (eds.) CiE 2008. LNCS, vol. 5028, pp. 359–369. Springer, Heidelberg (2008)
Pichardie, D., Rusu, V.: Defining and Reasoning About General Recursive Functions in Type Theory: A Practical Method. Research report, IRISA (2005)
Sozeau, M.: Subset coercions in coq. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 237–252. Springer, Heidelberg (2007)
Wadler, P.: Comprehending monads. MSCS (1992)
Whitman, P.: Free Lattices. Harvard University (1941)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
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: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds) Interactive Theorem Proving. ITP 2013. Lecture Notes in Computer Science, vol 7998. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39634-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-39634-2_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39633-5
Online ISBN: 978-3-642-39634-2
eBook Packages: Computer ScienceComputer Science (R0)