Constructive Galois connections
From MaRDI portal
Publication:4972068
Galois correspondences, closure operators (in relation to ordered sets) (06A15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
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 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; 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.
Recommendations
Cites work
- scientific article; zbMATH DE number 3910392 (Why is no real title available?)
- scientific article; zbMATH DE number 1324833 (Why is no real title available?)
- scientific article; zbMATH DE number 1953274 (Why is no real title available?)
- scientific article; zbMATH DE number 910715 (Why is no real title available?)
- scientific article; zbMATH DE number 1390341 (Why is no real title available?)
- A Calculational Approach to Control-Flow Analysis by Abstract Interpretation
- A Certified Lightweight Non-interference Java Bytecode Verifier
- A Galois connection calculus for abstract interpretation
- A category-theoretic account of program modules
- A certified denotational abstract interpreter
- Abstract interpretation and application to logic programs
- Abstracting gradual typing
- Calculating graph algorithms for dominance and shortest path
- Constructive Galois connections: taming the Galois connection framework for mechanized metatheory
- Extensible and efficient automation through reflective tactics
- Fiat: deductive synthesis of abstract data types in a proof assistant
- Grammar Analysis and Parsing by Abstract Interpretation
- Homotopy type theory. Univalent foundations of mathematics
- Hypercollecting semantics and its application to static analysis of information flow
- Program calculation in Coq
- Temporal abstract interpretation
- The octagon abstract domain
- ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
Cited in
(9)- scientific article; zbMATH DE number 1512777 (Why is no real title available?)
- Implication operators generating pairs of weak negations and their algebraic structure
- Faltings' construction of the K-Z connection
- Constructive Galois connections: taming the Galois connection framework for mechanized metatheory
- On constructivity of Galois connections
- Every Galois connection is the polarity of an antitone relation
- A Galois connection
- Foundations of dependent interoperability
- A Galois connection calculus for abstract interpretation
This page was built for publication: Constructive Galois connections
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4972068)
