Abstract
Current work on computational reflection is single-minded; each reflective procedure is written with a specific application or scope in mind. Composition of these reflective procedures is done by a proof- generating tactic language such as Ltac. This composition, however, comes at the cost of both larger proof terms and redundant preprocessing. In this work, we propose a methodology for writing composable reflective procedures that solve many small tasks in a single invocation. The key technical insights are techniques for reasoning semantically about extensible syntax in intensional type theory. Our techniques make it possible to compose sound procedures and write generic procedures parametrized by lemmas mimicking Coq’s support for hint databases.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006)
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)
Braibant, T., Pous, D.: Tactics for reasoning modulo AC in Coq. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 167–182. Springer, Heidelberg (2011)
Chlipala, A.: The Bedrock structured programming system: Combining generative metaprogramming and Hoare logic in an extensible program verifier. In: Proc. ICFP, pp. 391–402. ACM (2013)
Claret, G., del Carmen González Huesca, L., Régis-Gianas, Y., Ziliani, B.: Lightweight proof by reflection using a posteriori simulation of effectful computation. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 67–83. Springer, Heidelberg (2013)
Coq Development Team. The Coq proof assistant reference manual, version 8.4 (2012)
Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol. 1955, pp. 85–95. Springer, Heidelberg (2000)
Delaware, B., d.S. Oliveira, B.C., Schrijvers, T.: Meta-theory a la carte. SIGPLAN Not. 48(1), 207–218 (2013)
Garillot, F., Werner, B.: Simple types in type theory: Deep and shallow encodings. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 368–382. Springer, Heidelberg (2007)
Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq System. Rapport de recherche RR-6455, INRIA (2008)
Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: Proc. ICFP (2002)
Harper, R., Pollack, R.: Type checking with universes. Theoretical Computer Science 89(1), 107–136 (1991)
Hickey, J.J.: Formal objects in type theory using very dependent types. In: Foundations of Object Oriented Languages 3 (1996)
Lescuyer, S.: Formalisation et développement d’une tactique réflexive pour la démonstration automatique en Coq. Thèse de doctorat, Université Paris-Sud (January 2011)
Marti, N., Affeldt, R.: A certified verifier for a fragment of separation logic. Computer Software 25(3), 135–147 (2008)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. LICS, pp. 55–74. IEEE Computer Society (2002)
Stewart, G., Beringer, L., Appel, A.W.: Verified heap theorem prover by paramodulation. In: Proc. ICFP (2012)
Ziliani, B., Dreyer, D., Krishnaswami, N., Nanevski, A., Vafeiadis, V.: Mtac: A monad for typed tactic programming in Coq. In: Proc. ICFP (2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Malecha, G., Chlipala, A., Braibant, T. (2014). Compositional Computational Reflection. In: Klein, G., Gamboa, R. (eds) Interactive Theorem Proving. ITP 2014. Lecture Notes in Computer Science, vol 8558. Springer, Cham. https://doi.org/10.1007/978-3-319-08970-6_24
Download citation
DOI: https://doi.org/10.1007/978-3-319-08970-6_24
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08969-0
Online ISBN: 978-3-319-08970-6
eBook Packages: Computer ScienceComputer Science (R0)