On constructivity of Galois connections

DOI10.1007/978-3-319-73721-8_21MaRDI QIDQ3296346zbMATH OpenOpenAlexFDO

Authors Francesco Ranzato

Publication date 7 July 2020

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1704.08909, http://hdl.handle.net/11577/3258209

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) Semantics in the theory of computing (68Q55)

Abstract: Abstract interpretation-based static analyses rely on abstract domains of program properties, such as intervals or congruences for integer variables. Galois connections (GCs) between posets provide the most widespread and useful formal tool for mathematically specifying abstract domains. Recently, Darais and Van Horn [2016] put forward a notion of constructive Galois connection for unordered sets (rather than posets), which allows to define abstract domains in a so-called mechanized and calculational proof style and therefore enables the use of proof assistants like Coq and Agda for automatically extracting verified algorithms of static analysis. We show here that constructive GCs are isomorphic, in a precise and comprehensive meaning including sound abstract functions, to so-called partitioning GCs--an already known class of GCs which allows to cast standard set partitions as an abstract domain. Darais and Van Horn [2016] also provide a notion of constructive GC for posets, which we prove to be isomorphic to plain GCs and therefore lose their constructive attribute. Drawing on these findings, we put forward and advocate the use of purely partitioning GCs, a novel class of constructive abstract domains for a mechanized approach to abstract interpretation. We show that this class of abstract domains allows us to represent a set partition with more flexibility while retaining a constructive approach to Galois connections.

Recommendations

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

Cited in

(10)

• scientific article; zbMATH DE number 1512777 (Why is no real title available?)
• A Galois connection related to restrictions of continuous real functions
• Constructive Galois connections
• Safety of abstract interpretations for free, via logical relations and Galois connections
• Partial approximative set theory: a view from Galois connections
• scientific article; zbMATH DE number 797421 (Why is no real title available?)
• A Galois connection approach to superposition and inaccessibility
• Constructive Galois connections: taming the Galois connection framework for mechanized metatheory
• scientific article; zbMATH DE number 2149938 (Why is no real title available?)
• A Galois connection calculus for abstract interpretation

This page was built for publication: On constructivity of Galois connections

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3296346)