Hostname: page-component-586b7cd67f-r5fsc Total loading time: 0 Render date: 2024-11-28T15:01:32.097Z Has data issue: false hasContentIssue false
  • English
  • Français

Constructive Galois Connections

Part of: JFP Research Articles

Published online by Cambridge University Press:  08 July 2019

DAVID DARAIS  and
DAVID VAN HORN
DAVID DARAIS
Affiliation:
University of Vermont, USA (e-mail: [email protected])
DAVID VAN HORN
Affiliation:
University of Maryland, College Park, USA (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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 using proof assistants 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 connections, 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: the first uses calculational abstract interpretation to design a static analyzer, and the second 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.

Type
Regular Paper
Information
Journal of Functional Programming , Volume 29 , 2019 , e11
Copyright
© Cambridge University Press 2019 

References

Assaf, M., Naumann, D. A., Signoles, J., Totel, É., & Tronel, F. (2017). Hypercollecting semantics and its application to static analysis of information flow. In Principles of Programming Languages (POPL). New York, NY, USA: ACM.Google Scholar
Barthe, G., Pichardie, D., & Rezk, T. (2007). A certified lightweight non-interference Java bytecode verifier. In European Symposium on Programming (ESOP). Berlin, Heidelberg: Springer-Verlag.Google Scholar
Bird, R. (1990). A calculus of functions for program derivation. In Research Topics in Functional Programming. Boston, MA, USA: Addison-Wesley Longman Publishing Co.Google Scholar
Bird, R. & de Moor, O. (1996). The algebra of programming. Upper Saddle River, NJ, USA: Prentice Hall.CrossRefGoogle Scholar
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., & Rival, X. (2003). A static analyzer for large safety-critical software. InProgramming Language Design and Implementation (PLDI). New York, NY, USA: ACM.Google Scholar
Blazy, S., Laporte, V., Maroneze, A., & Pichardie, D. (2013). Formal verification of a C value analysis based on abstract interpretation. In Static Analysis Symposium (SAS). Berlin, Heidelberg: Springer-Verlag.Google Scholar
Cachera, D. & Pichardie, D. (2010). A certified denotational abstract interpreter. Interactive Theorem Proving (ITP). Berlin, Heidelberg: Springer-Verlag.Google Scholar
Cousot, P. (1999). The calculational design of a generic abstract interpreter. In Calculational System Design. NATO ASI Series F. Amsterdam: IOS Press.Google Scholar
Cousot, P. (2005). Abstract interpretation. MIT course 16.399, http://web.mit.edu/16.399/ www/.Google Scholar
Cousot, P. (2008). Abstract interpretation. http://www.di.ens.fr/~cousot/AI/.Google Scholar
Cousot, P. & Cousot, R. (1976). Static determination of dynamic properties of programs. In International Symposium on Programming (ISOP). Paris, France: Dunod.Google Scholar
Cousot, P. & Cousot, R. (1977). Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Principles of Programming Languages (POPL). New York, NY, USA: ACM.Google Scholar
Cousot, P. & Cousot, R. (1979). Systematic design of program analysis frameworks. In Principles of Programming Languages (POPL). New York, NY, USA: ACM.Google Scholar
Cousot, P. & Cousot, R. (1992). Inductive definitions, semantics and abstract interpretations. In Principles of Programming Languages (POPL). New York, NY, USA: ACM.Google Scholar
Cousot, P. & Cousot, R. (1994). Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages), invited paper. In International Conference on Computer Languages (ICCL). Los Alamitos, CA, USA: IEEE Computer Society Press, pp. 95–112.Google Scholar
Cousot, P. & Cousot, R. (2014). A Galois connection calculus for abstract interpretation. In Principles of Programming Languages (POPL). New York, NY, USA: ACM.Google Scholar
Cousot, P. & Halbwachs, N. (1978). Automatic discovery of linear restraints among variables of a program. In Principles of Programming Languages (POPL). New York, NY, USA: ACM.Google Scholar
Danielsson, N. A., Norell, U., Mu, S. C., Bronson, S., Doel, D., Jansson, P., & Chen, L. T. (2011). The Agda standard library. Url: http://www.cs.nott.ac.uk/~nad/repos/lib.Google Scholar
Darais, D. & Van Horn, D. (2016). Constructive Galois connections: Taming the Galois connection framework for mechanized metatheory. In International Conference on Functional Programming (ICFP). New York, NY, USA: ACM.Google Scholar
Darais, D., Might, M., & Van Horn, D. (2015). Galois transformers and modular abstract interpreters: Reusable metatheory for program analysis. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). New York, NY, USA: ACM.Google Scholar
Delaware, B., Pit-Claudel, C., Gross, J., & Chlipala, A. (2015). Fiat: Deductive synthesis of abstract data types in a proof assistant. In Principles of Programming Languages (POPL). New York, NY, USA: ACM.Google Scholar
Garcia, R., Clark, A. M., & Tanter, É. (2016). Abstracting gradual typing. In Principles of Programming Languages (POPL). New York, NY, USA: ACM.Google Scholar
Jourdan, J.-H., Laporte, V., Blazy, S., Leroy, X., & Pichardie, D. (2015). A formally-verified C static analyzer. In Principles of Programming Languages (POPL). New York, NY, USA: ACM.Google Scholar
Leroy, X. (2009). Formal verification of a realistic compiler. In Communications of the ACM (CACM). New York, NY, USA: ACM.Google Scholar
Malecha, G. & Bengtson, J. (2016). Extensible and efficient automation through reflective tactics. In Programming Languages and Systems (PLAS). New York, NY, USA: Springer-Verlag.Google Scholar
Martin-Löf, P. (1984). Intuitionistic type theory. Studies in proof theory. Naples, Italy: Bibliopolis.Google Scholar
Midtgaard, J. & Jensen, T. (2008). A calculational approach to control-flow analysis by abstract interpretation. In Static Analysis Symposium (SAS). Berlin, Heidelberg: Springer-Verlag.Google Scholar
Miné, A. (2006). The octagon abstract domain. In Higher Order and Symbolic Computation (HOSC). Hingham, MA, USA: Kluwer Academic Publishers.Google Scholar
Moggi, E. (1989). An abstract view of programming languages. Tech. rept. University of Edinburgh.Google Scholar
Monniaux, D. (1998). Réalisation mécanisée d’interpréteurs abstraits. Rapport de DEA, Université Paris VII. In French.Google Scholar
Nielson, F, Nielson, H. R., & Hankin, C. (1999). Principles of program analysis. New York, NY, USA: Springer-Verlag.CrossRefGoogle Scholar
Norell, U. (2007). Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology.Google Scholar
Pichardie, D. (2005). Interprétation abstraite en logique intuitionniste: Extraction d’analyseurs Java certifiés. PhD thesis, Université Rennes 1. In French.Google Scholar
Scott, D. (1975). Data types as lattices. ISILC Logic Conference. Berlin, Heidelberg: Springer Berlin Heidelberg.Google Scholar
Sergey, I., Midtgaard, J., & Clarke, D. (2012). Calculating graph algorithms for dominance and shortest path. In Mathematics of Program Construction (MPC). Berlin, Heidelberg: Springer-Verlag.Google Scholar
Sergey, I., Devriese, D., Might, M., Midtgaard, J., Darais, D., Clarke, D., & Piessens, F. (2013). Monadic abstract interpreters. In Programming Language Design and Implementation (PLDI). New York, NY, USA: ACM.Google Scholar
Silva, P. F., & Oliveira, J. N. (2008). Galculator: Functional prototype of a Galois-connection based proof assistant. In Principles and Practice of Declarative Programming (PPDP). New York, NY, USA: ACM.Google Scholar
Tesson, J., Hashimoto, H., Hu, Z., Loulergue, F., & Takeichi, M. (2011). Program calculation in Coq. In Algebraic Methodology and Software Technology (AMAST). Berlin, Heidelberg: Springer-Verlag.Google Scholar
The Univalent Foundations Program. (2013). Homotopy type theory: Univalent foundations of mathematics. Institute for Advanced Study. https://homotopytypetheory.org/book.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.