David Darais
David Van Horn
ABSTRACT
Galois connections are a foundational tool for structuring abstraction in semantics and their use lies at the heart of the theory of abstract interpretation. Yet, mechanization of Galois connections remains limited to restricted modes of use, preventing their general application in mechanized metatheory and certified programming.
This paper presents constructive Galois connections, a variant of Galois connections that is effective both on paper and in proof assistants; is complete with respect to a large subset of classical Galois connections; and enables more general reasoning principles, including the "calculational" style advocated by Cousot.
To design constructive Galois connection we identify a restricted mode of use of classical ones which is both general and amenable to mechanization in dependently-typed functional programming languages. Crucial to our metatheory is the addition of monadic structure to Galois connections to control a "specification effect". Effectful calculations may reason classically, while pure calculations have extractable computational content. Explicitly moving between the worlds of specification and implementation is enabled by our metatheory.
To validate our approach, we provide two case studies in mechanizing existing proofs from the literature: one uses calculational abstract interpretation to design a static analyzer, the other forms a semantic basis for gradual typing. Both mechanized proofs closely follow their original paper-and-pencil counterparts, employ reasoning principles not captured by previous mechanization approaches, support the extraction of verified algorithms, and are novel.
- G. Barthe, D. Pichardie, and T. Rezk. A certified lightweight noninterference java bytecode verifier. In R. D. Nicola, editor, Programming Languages and Systems, Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2007. Google Scholar
Digital Library
- R. Bird and O. de Moor. The Algebra of Programming. Prentice Hall, 1996. Google ScholarDigital Library
- R. S. Bird. A calculus of functions for program derivation. In D. A. Turner, editor, Research Topics in Functional Programming. Addison-Wesley, 1990. Also available as Technical Monograph PRG-64, from the Programming Research Group, Oxford University. Google ScholarDigital Library
- B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’03. ACM, 2003. Google ScholarDigital Library
- S. Blazy, V. Laporte, A. Maroneze, and D. Pichardie. Formal verification of a c value analysis based on abstract interpretation. In F. Logozzo and M. Fähndrich, editors, Static Analysis, Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2013.Google Scholar
- D. Cachera and D. Pichardie. A certified denotational abstract interpreter. In M. Kaufmann and L. Paulson, editors, Interactive Theorem Proving, Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2010. Google ScholarDigital Library
- P. Cousot. Abstract interpretation.Google Scholar
- P. Cousot. The calculational design of a generic abstract interpreter. In M. Broy and R. Steinbrüggen, editors, Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam, 1999.Google Scholar
- P. Cousot. MIT 16.399: Abstract interpretation, 2005.Google Scholar
- P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In 2nd International Symposium on Programming, 1976.Google Scholar
- P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. ACM, 1977. Google ScholarDigital Library
- P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’79. ACM, 1979. Google ScholarDigital Library
- P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretations. In Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’92. ACM, 1992. Google ScholarDigital Library
- P. Cousot and R. Cousot. A Galois connection calculus for abstract interpretation. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14. ACM, 2014. Google ScholarDigital Library
- D. Darais, M. Might, and D. Van Horn. Galois transformers and modular abstract interpreters. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, pages 552–571. ACM, 2015. Google ScholarDigital Library
- B. Delaware, C. Pit-Claudel, J. Gross, and A. Chlipala. Fiat: Deductive synthesis of abstract data types in a proof assistant. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015. ACM, 2015. Google ScholarDigital Library
- R. Garcia, A. M. Clark, and É. Tanter. Abstracting gradual typing. In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), St Petersburg, FL, USA, Jan. 2016. ACM Press. To appear. Google ScholarDigital Library
- J. H. Jourdan, V. Laporte, S. Blazy, X. Leroy, and D. Pichardie. A Formally-Verified c static analyzer. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’15. ACM, 2015. Google ScholarDigital Library
- X. Leroy. Formal verification of a realistic compiler. Commun. ACM, 2009. Google ScholarDigital Library
- G. Malecha and J. Bengtson. Extensible and efficient automation through reflective tactics. In Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016. Springer, 2016.Google Scholar
- P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.Google Scholar
- J. Midtgaard and T. Jensen. A calculational approach to Control-Flow analysis by abstract interpretation. In M. Alpuente and G. Vidal, editors, Static Analysis, Lecture Notes in Computer Science, chapter 23. Springer Berlin Heidelberg, 2008. Google ScholarDigital Library
- J. Midtgaard and T. Jensen. A calculational approach to Control-Flow analysis by abstract interpretation. In M. Alpuente and G. Vidal, editors, Static Analysis Symposium, LNCS. Springer, 2008. Google ScholarDigital Library
- A. Miné. The octagon abstract domain. Higher-Order and Symbolic Computation, 2006. Google ScholarDigital Library
- E. Moggi. An abstract view of programming languages. Technical report, Edinburgh University, 1989.Google Scholar
- D. Monniaux. Réalisation mécanisée d’interpréteurs abstraits. Rapport de DEA, Université Paris VII, 1998. French.Google Scholar
- F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag, 1999. Google ScholarDigital Library
- U. Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden, Sept. 2007.Google Scholar
- D. Pichardie. Interprétation abstraite en logique intuitionniste: extraction d’analyseurs Java certifiés. PhD thesis, Université Rennes, 2005.Google Scholar
- I. Sergey, J. Midtgaard, and D. Clarke. Calculating graph algorithms for dominance and shortest path. In J. Gibbons and P. Nogueira, editors, Mathematics of Program Construction, Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2012. Google ScholarDigital Library
- I. Sergey, D. Devriese, M. Might, J. Midtgaard, D. Darais, D. Clarke, and F. Piessens. Monadic abstract interpreters. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 2013. Google ScholarDigital Library
- P. F. Silva and J. N. Oliveira. ‘Galculator’: Functional prototype of a Galois-connection based proof assistant. In Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP ’08. ACM, 2008. Google ScholarDigital Library
- J. Tesson, H. Hashimoto, Z. Hu, F. Loulergue, and M. Takeichi. Program calculation in Coq. In M. Johnson and D. Pavlovic, editors, Algebraic Methodology and Software Technology, Lecture Notes in Computer Science, chapter 10. Springer Berlin Heidelberg, 2011. Google ScholarDigital Library
Index Terms
- Constructive Galois connections: taming the Galois connection framework for mechanized metatheory
Recommendations
Constructive Galois connections: taming the Galois connection framework for mechanized metatheory
ICFP '16Galois connections are a foundational tool for structuring abstraction in semantics and their use lies at the heart of the theory of abstract interpretation. Yet, mechanization of Galois connections remains limited to restricted modes of use, ...
Logics from Galois connections
In this paper, Information Logic of Galois Connections (ILGC) suited for approximate reasoning about knowledge is introduced. In addition to the three classical propositional logic axioms and the inference rule of modus ponens, ILGC contains only two ...
Galois transformers and modular abstract interpreters: reusable metatheory for program analysis
OOPSLA 2015: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and ApplicationsThe design and implementation of static analyzers has become increasingly systematic. Yet for a given language or analysis feature, it often requires tedious and error prone work to implement an analyzer and prove it sound. In short, static analysis ...
Comments