research-article

Public Access

Constructive Galois connections: taming the Galois connection framework for mechanized metatheory

Authors:

David Van HornAuthors Info & Claims

ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming

Pages 311 - 324

https://doi.org/10.1145/2951913.2951934

Published: 04 September 2016 Publication History

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.

References

[1]

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.

Digital Library

[2]

R. Bird and O. de Moor. The Algebra of Programming. Prentice Hall, 1996.

Digital Library

[3]

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.

Digital Library

[4]

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.

Digital Library

[5]

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.

[6]

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.

Digital Library

[7]

P. Cousot. Abstract interpretation.

[8]

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.

[9]

P. Cousot. MIT 16.399: Abstract interpretation, 2005.

[10]

P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In 2nd International Symposium on Programming, 1976.

[11]

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.

Digital Library

[12]

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.

Digital Library

[13]

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.

Digital Library

[14]

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.

Digital Library

[15]

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.

Digital Library

[16]

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.

Digital Library

[17]

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.

Digital Library

[18]

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.

Digital Library

[19]

X. Leroy. Formal verification of a realistic compiler. Commun. ACM, 2009.

Digital Library

[20]

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.

[21]

P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.

[22]

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.

Digital Library

[23]

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.

Digital Library

[24]

A. Miné. The octagon abstract domain. Higher-Order and Symbolic Computation, 2006.

Digital Library

[25]

E. Moggi. An abstract view of programming languages. Technical report, Edinburgh University, 1989.

[26]

D. Monniaux. Réalisation mécanisée d’interpréteurs abstraits. Rapport de DEA, Université Paris VII, 1998. French.

[27]

F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag, 1999.

Digital Library

[28]

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.

[29]

D. Pichardie. Interprétation abstraite en logique intuitionniste: extraction d’analyseurs Java certifiés. PhD thesis, Université Rennes, 2005.

[30]

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.

Digital Library

[31]

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.

Digital Library

[32]

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.

Digital Library

[33]

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.

Digital Library

Cited By

Michelland SZakowski YGonnord L(2024)Abstract Interpreters: A Monadic Approach to Modular VerificationProceedings of the ACM on Programming Languages10.1145/36746468:ICFP(602-629)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674646
Near JDarais DAbuah CStevens TGaddamadugu PWang LSomani NZhang MSharma NShan ASong D(2019)Duet: an expressive higher-order language and linear type system for statically enforcing differential privacyProceedings of the ACM on Programming Languages10.1145/33605983:OOPSLA(1-30)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360598
Wang SCao QMohan AHobor A(2019)Certifying graph-manipulating C programs via localizations within data structuresProceedings of the ACM on Programming Languages10.1145/33605973:OOPSLA(1-30)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360597
Show More Cited By

Index Terms

Constructive Galois connections: taming the Galois connection framework for mechanized metatheory
1. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

Constructive Galois connections: taming the Galois connection framework for mechanized metatheory
ICFP '16

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, ...
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 Applications

The 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming

September 2016

501 pages

ISBN:9781450342193

DOI:10.1145/2951913

General Chairs:
Jacques Garrigue
Nagoya University, Japan
,
Gabriele Keller
University of New South Wales, Australia
,
Program Chair:
Eijiro Sumii
Tohoku University, Japan

ACM SIGPLAN Notices Volume 51, Issue 9
ICFP '16
September 2016
501 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/3022670
Editor:
Matthew Fluet
Issue’s Table of Contents

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 September 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

DARPA

Conference

ICFP'16

Sponsor:

SIGPLAN

ICFP'16: ACM SIGPLAN International Conference on Functional Programming

September 18 - 24, 2016

Nara, Japan

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
576
Total Downloads

Downloads (Last 12 months)102
Downloads (Last 6 weeks)25

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Michelland SZakowski YGonnord L(2024)Abstract Interpreters: A Monadic Approach to Modular VerificationProceedings of the ACM on Programming Languages10.1145/36746468:ICFP(602-629)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674646
Near JDarais DAbuah CStevens TGaddamadugu PWang LSomani NZhang MSharma NShan ASong D(2019)Duet: an expressive higher-order language and linear type system for statically enforcing differential privacyProceedings of the ACM on Programming Languages10.1145/33605983:OOPSLA(1-30)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360598
Wang SCao QMohan AHobor A(2019)Certifying graph-manipulating C programs via localizations within data structuresProceedings of the ACM on Programming Languages10.1145/33605973:OOPSLA(1-30)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360597
Zuriel YFriedman MSheffi GCohen NPetrank E(2019)Efficient lock-free durable setsProceedings of the ACM on Programming Languages10.1145/33605543:OOPSLA(1-26)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360554
Henriksen IBilardi GPingali K(2019)Derivative grammars: a symbolic approach to parsing with derivativesProceedings of the ACM on Programming Languages10.1145/33605533:OOPSLA(1-28)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360553
Wei GChen YRompf T(2019)Staged abstract interpreters: fast and modular whole-program analysis via meta-programmingProceedings of the ACM on Programming Languages10.1145/33605523:OOPSLA(1-32)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360552
Ricciotti WStolarek JPerera RCheney J(2017)Imperative functional programs that explain their workProceedings of the ACM on Programming Languages10.1145/31102581:ICFP(1-28)Online publication date: 29-Aug-2017
https://dl.acm.org/doi/10.1145/3110258
Cabrera ICordero POjeda-Aciego M(2017)Galois connections in computational intelligence: A short survey2017 IEEE Symposium Series on Computational Intelligence (SSCI)10.1109/SSCI.2017.8285310(1-7)Online publication date: Nov-2017
https://doi.org/10.1109/SSCI.2017.8285310
Ranzato F(2017)On Constructivity of Galois ConnectionsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-319-73721-8_21(452-473)Online publication date: 29-Dec-2017
https://doi.org/10.1007/978-3-319-73721-8_21

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents