Jael Kriener
Sandrine Blazy
ABSTRACT
Basing program analyses on formal semantics has a long and successful tradition in the logic programming paradigm. These analyses rely on results about the relative correctness of mathematically sophisticated semantics, and authors of such analyses often invest considerable effort into establishing these results. The development of interactive theorem provers such as Coq and their recent successes both in the field of program verification as well as in mathematics, poses the question whether these tools can be usefully deployed in logic programming. This paper presents formalisations in Coq of several general results about the correctness of semantics in different styles; forward and backward, top-down and bottom-up. The results chosen are paradigmatic of the kind of correctness theorems that semantic analyses rely on and are therefore well-suited to explore the possibilities afforded by the application of interactive theorem provers to this task, as well as the difficulties likely to be encountered in the endeavour. It turns out that the advantages offered by moving to a functional setting, including the possibility to apply higher-order abstract syntax, are considerable.
- {Abramsky and Hankin, 1987} Abramsky, S. and Hankin, C. (1987). Abstract Interpretation of Declarative Languages. Ellis Horwood. Google Scholar
Digital Library
- {Abramsky and Jung, 1994} Abramsky, S. and Jung, A. (1994). Domain theory. In Abramsky, S., Gabbay, D., and Maibaum, T. S. E., editors, Handbook of Logic in Computer Science, pages 1--168. Oxford University Press. Google ScholarDigital Library
- {Barbuti et al., 1993} Barbuti, R., Giacobazzi, R., and Levi, G. (1993). A General Framework for Semantics-Based Bottom-Up Abstract Interpretation of Logic Programs. ACM TOPLAS, 15(1):133--181. Google ScholarDigital Library
- {Benton et al., 2009} Benton, N., Kennedy, A., and Varming, C. (2009). Some Domain Theory and Denotational Semantics in Coq. In {Berghofer et al., 2009}, pages 115--130. Google ScholarDigital Library
- {Berghofer et al., 2009} Berghofer, S., Nipkow, T., Urban, C., and Wenzel, M., editors (2009). Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17--20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science. Springer. Google ScholarDigital Library
- {Bertot and Komendantsky, 2008} Bertot, Y. and Komendantsky, V. (2008). Fixed point semantics and partial recursion in Coq. In Antoy, S. and Albert, E., editors, PPDP, pages 89--96. ACM. Google ScholarDigital Library
- {Besson et al., 2009} Besson, F., Cachera, D., Jensen, T. P., and Pichardie, D. (2009). Certified Static Analysis by Abstract Interpretation. In FOSAD, volume 5705 of LNCS, pages 223--257. Springer. Google ScholarDigital Library
- {Besson et al., 2006} Besson, F., Jensen, T. P., and Pichardie, D. (2006). Proof-carrying code from certified abstract interpretation and fixpoint compression. TCS, 364(3):273--291. Google ScholarDigital Library
- {Billaud, 1990} Billaud, M. (1990). Simple Operational and Denotational Semantics for Prolog with Cut. Theoretical Computer Science, 71(2):193--208. Google ScholarDigital Library
- {Birkhoff, 1967} Birkhoff, G. (1967). Lattice Theory. In Colloquium Publications, volume 25. Amererican Mathematical Society, 3. edition.Google Scholar
- {Blanqui and Koprowski, 2011} Blanqui, F. and Koprowski, A. (2011). CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Mathematical Structures in Computer Science, 21(4):827--859.Google ScholarCross Ref
- {Bruijn, 1972} Bruijn, N. G. D. (1972). Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. INDAG. MATH, 34:381--392.Google ScholarCross Ref
- {Cachera et al., 2005} Cachera, D., Jensen, T. P., Pichardie, D., and Rusu, V. (2005). Extracting a data flow analyser in constructive logic. TCS, 342(1):56--78. Google ScholarDigital Library
- {Cachera and Pichardie, 2010} Cachera, D. and Pichardie, D. (2010). A certified denotational abstract interpreter. In Proc. of the conference on Interactive Theorem Proving (ITP-10), volume 6172 of Lecture Notes in Computer Science, pages 9--24. Springer-Verlag. Google ScholarDigital Library
- {Cheney and Urban, 2004} Cheney, J. and Urban, C. (2004). αProlog: A Logic Programming Language with Names, Binding and α-Equivalence. In Demoen, B. and Lifschitz, V., editors, ICLP, volume 3132 of Lecture Notes in Computer Science, pages 269--283. Springer.Google Scholar
- {Chlipala, 2008} Chlipala, A. (2008). Parametric higher-order abstract syntax for mechanized semantics. In Hook, J. and Thiemann, P., editors, ICFP, pages 143--156. ACM. Google ScholarDigital Library
- {Codish et al., 1994} Codish, M., Dams, D., and Yardeni, E. (1994). Bottom-up Abstract Interpretation of Logic Programs. Theoretical Computer Science, 124(1):93--125. Google ScholarDigital Library
- {CompCert Development Team, 2012} CompCert Development Team (2012). The CompCert formally verified C compiler. http://compcert.inria.fr/.Google Scholar
- {Coq Development Team, 2010} Coq Development Team (2010). The Coq Proof Assistant Reference Manual, Version 8.3. INRIA. http://coq.inria.fr/refman/.Google Scholar
- {Cousot and Cousot, 1979} Cousot, P. and Cousot, R. (1979). Systematic Design of Program Analysis Frameworks. In POPL, pages 269--282. ACM Press. Google ScholarDigital Library
- {de la Banda et al., 1996} de la Banda, M. J. G., Hermenegildo, M. V., Bruynooghe, M., Dumortier, V., Janssens, G., and Simoens, W. (1996). Global Analysis of Constraint Logic Programs. ACM Trans. Program. Lang. Syst., 18(5):564--614. Google ScholarDigital Library
- {de Vink, 1989} de Vink, E. P. (1989). Comparative Semantics for Prolog with Cut. Science of Computer Programming, 13(1):237--264. Google ScholarDigital Library
- {Debray and Mishra, 1988} Debray, S. K. and Mishra, P. (1988). Denotational and Operational Semantics for Prolog. Journal of Logic Programming, 5(1):81--91. Google ScholarDigital Library
- {Drabent, 2012} Drabent, W. (2012). A Simple Correctness Proof for Magic Transformation. Theory and Practice of Logic Programming, 12:929--936. Google ScholarDigital Library
- {Felty et al., 1988} Felty, A. P., Gunter, E. L., Hannan, J., Miller, D., Nadathur, G., and Scedrov, A. (1988). Lambda-Prolog: An Extended Logic Programming Language. In Lusk, E. L. and Overbeek, R. A., editors, CADE, volume 310 of Lecture Notes in Computer Science, pages 754--755. Springer. Google ScholarDigital Library
- {Gabbrielli and Levi, 1991} Gabbrielli, M. and Levi, G. (1991). On the Semantics of Logic Programs. In ICALP, volume 510 of LNCS, pages 1--19. Springer. Google ScholarDigital Library
- {Gallagher, 2003} Gallagher, J. P. (2003). A Program Transformation for Backwards Analysis of Logic Programs. In Bruynooghe, M., editor, LOPSTR, volume 3018 of Lecture Notes in Computer Science, pages 92--105. Springer.Google Scholar
- {Giacobazzi, 1993} Giacobazzi, R. (1993). Semantic Aspects of Logic Program Analysis. PhD thesis, Dipartimento di Informatica, Università di Pisa.Google Scholar
- {Gonthier, 2007} Gonthier, G. (2007). The Four Colour Theorem: Engineering of a Formal Proof. In Kapur, D., editor, ASCM, volume 5081 of LNCS, page 333. Springer. Google ScholarDigital Library
- {Gonthier et al., 2013} Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Roux, S. L., Mahboubi, A., O'Connor, R., Biha, S. O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., and Thery, L. (2013). A machine-checked proof of the odd order theorem. In Proc. of the 4th conference on Interactive Theorem Proving, volume 7998 of Lecture Notes in Computer Science, pages 163--179, Rennes, France. Springer. Google ScholarDigital Library
- {Gonthier and Mahboubi, 2010} Gonthier, G. and Mahboubi, A. (2010). An introduction to small scale reflection in Coq. Journal of Formalised Reasoning, 3(2):95--152.Google Scholar
- {Hudak, 1987} Hudak, P. (1987). A Semantic Model of Reference Counting and its Abstraction. In Abstract Interpretation of Declarative Languages, pages 45--62. Ellis Horwood.Google Scholar
- {Janssens and Bruynooghe, 1992} Janssens, G. and Bruynooghe, M. (1992). Deriving Descriptions of Possible Values of Program Variables by Means of Abstract Interpretation. JLP, 13(2&3):205--258. Google ScholarDigital Library
- {King and Lu, 2002} King, A. and Lu, L. (2002). A Backward Analysis for Constraint Logic Programs. TPLP, 2(4-5):517--547. Google ScholarDigital Library
- {King and Lu, 2003} King, A. and Lu, L. (2003). Forward versus Backward Verification of Logic Programs. In ICLP, volume 2916 of LNCS, pages 315--330. Springer.Google Scholar
- {Kleene, 1938} Kleene, S. C. (1938). On notation for ordinal numbers. The Journal of Symbolic Logic, 3(4):pp. 150--155.Google ScholarCross Ref
- {Klein et al., 2010} Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., and Winwood, S. (2010). SeL4: formal verification of an operating-system kernel. CACM, 53(6):107--115. Google ScholarDigital Library
- {Kriener and King, 2011} Kriener, J. and King, A. (2011). RedAlert: Determinacy inference for Prolog. TPLP, 11(4-5):537--553. Proofs in CoRR volume abs/1109.2548 at http://arxiv.org/abs/1109.2548.Google ScholarCross Ref
- {Leroy, 2009} Leroy, X. (2009). Formal verification of a realistic compiler. CACM, 52(7):107--115. Google ScholarDigital Library
- {Levi, 1991} Levi, G. (1991). On the Semantics of Logic Programs. In ICLP, page 945. MIT Press.Google Scholar
- {Muthukumar and Hermenegildo, 1992} Muthukumar, K. and Hermenegildo, M. V. (1992). Compile-Time Derivation of Variable Dependency Using Abstract Interpretation. JLP, 13(2&3):315--347. Google ScholarDigital Library
- {Pfenning and Elliott, 1988} Pfenning, F. and Elliott, C. (1988). Higher-Order Abstract Syntax. In Wexelblat, R. L., editor, PLDI, pages 199--208. ACM. Google ScholarDigital Library
- {Pusch, 1996} Pusch, C. (1996). Verification of Compiler Correctness for the WAM. In TPHOLs, volume 1125 of LNCS, pages 347--361. Springer. Google ScholarDigital Library
- {Ramakrishnan, 1991} Ramakrishnan, R. (1991). Magic templates: A spellbinding approach to logic programs. J. Log. Program., 11(3&4):189--216. Google ScholarDigital Library
- {Schrijvers et al., 2005} Schrijvers, T., Stuckey, P. J., and Duck, G. J. (2005). Abstract interpretation for constraint handling rules. In Barahona, P. and Felty, A. P., editors, PPDP, pages 218--229. ACM. Google ScholarDigital Library
- {Schürmann, 2009} Schürmann, C. (2009). The Twelf Proof Assistant. In {Berghofer et al., 2009}, pages 79--83. Google ScholarDigital Library
- {Scott, 1971} Scott, D. (1971). Continuous lattices. Technical Report PRG07, OUCL.Google Scholar
- {Tarski, 1955} Tarski, A. (1955). A Lattice-Theoretical Fixpoint Theorem and its Applications. Pacific Journal of Mathematics, 5(2):285--309.Google ScholarCross Ref
- {van Emden and Kowalski, 1976} van Emden, M. H. and Kowalski, R. A. (1976). The Semantics of Predicate Logic as a Programming Language. JACM, 23(4):733--742. Google ScholarDigital Library
Index Terms
- Proofs you can believe in: proving equivalences between Prolog semantics in Coq
Recommendations
Interactive proofs in higher-order concurrent separation logic
POPL '17When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...
Interactive proofs in higher-order concurrent separation logic
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesWhen using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...
Completeness and Decidability Results for CTL in Constructive Type Theory
We prove completeness and decidability results for the temporal logic CTL in Coq/Ssreflect. Our main result is a constructive proof that for every formula one can obtain either a finite model satisfying the formula or a proof in a Hilbert system ...
Comments