On constructivity of Galois connections. (English) Zbl 1446.68035

Dillig, Isil (ed.) et al., Verification, model checking, and abstract interpretation. 19th international conference, VMCAI 2018, Los Angeles, CA, USA, January 7–9, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10747, 452-473 (2018).
Summary: 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. D. Darais and D. Van Horn [in: Proceedings of the 21st ACM SIGPLAN international conference on functional programming, ICFP’16. New York, NY: Association for Computing Machinery (ACM). 311–324 (2016; Zbl 1361.68129)] 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 certified algorithms of static analysis. We show here that constructive GCs are isomorphic, in a mathematical meaning which includes 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 [loc. cit.] further provide a notion of constructive Galois connection for posets, which we prove to be mathematically isomorphic to plain GCs. Drawing on these findings, we put forward 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 in a flexible way while retaining a constructive approach to Galois connections.
For the entire collection see [Zbl 1409.68012].


68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
06A15 Galois correspondences, closure operators (in relation to ordered sets)
68Q55 Semantics in the theory of computing


Zbl 1361.68129
Full Text: DOI arXiv Link