Constructive Galois connections

DOI10.1017/S0956796819000066zbMATH Open1493.68104arXiv1807.08711OpenAlexW2963650512WikidataQ127545096 ScholiaQ127545096MaRDI QIDQ4972068FDOQ4972068

David van Horn, David Darais

Publication date: 22 November 2019

Published in: Journal of Functional Programming (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1807.08711

Recommendations

• Constructive Galois connections: taming the Galois connection framework for mechanized metatheory
• On constructivity of Galois connections
• A Galois connection calculus for abstract interpretation
• scientific article; zbMATH DE number 2090019
• Galois Connections for Recursive Types

Mathematics Subject Classification ID

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)

Cites Work

• Title not available (Why is that?)
• The octagon abstract domain
• Fiat: deductive synthesis of abstract data types in a proof assistant
• Title not available (Why is that?)
• Title not available (Why is that?)
• Abstract interpretation and application to logic programs
• A category-theoretic account of program modules
• Homotopy Type Theory: Univalent Foundations of Mathematics
• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
• Grammar Analysis and Parsing by Abstract Interpretation
• A certified denotational abstract interpreter
• Temporal abstract interpretation
• Title not available (Why is that?)
• A Certified Lightweight Non-interference Java Bytecode Verifier
• Title not available (Why is that?)
• Hypercollecting semantics and its application to static analysis of information flow
• Calculating Graph Algorithms for Dominance and Shortest Path
• A galois connection calculus for abstract interpretation
• A Calculational Approach to Control-Flow Analysis by Abstract Interpretation
• Abstracting gradual typing
• Extensible and Efficient Automation Through Reflective Tactics
• Program calculation in Coq
• Constructive Galois connections: taming the Galois connection framework for mechanized metatheory

Cited In (5)

• Title not available (Why is that?)
• Implication operators generating pairs of weak negations and their algebraic structure
• Faltings' construction of the K-Z connection
• Every Galois connection is the polarity of an antitone relation
• A Galois connection

Uses Software

• Galculator
• ASTREE
• Verasco
• Fiat

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)