Skip to main content

A Galois connection calculus for abstract interpretation

Patrick Cousot, Radhia Cousot

DOI 10.1145/2535838.2537850 dblp BibTeX

Abstract

We introduce a Galois connection calculus for language independent specification of abstract interpretations used in programming language semantics, formal verification, and static analysis. This Galois connection calculus and its type system are typed by abstract interpretation.

Related papers

Domain Precision in Galois Connection-Less Abstract Interpretation SAS 2023
Constructive Galois connections: taming the Galois connection framework for mechanized metatheory ICFP 2016
Constructive Galois Connections JFP 2019
Types as Abstract Interpretations POPL 1997
Galois transformers and modular abstract interpreters: reusable metatheory for program analysis OOPSLA 2015
Transport via Partial Galois Connections and Equivalences APLAS 2023
Quantum abstract interpretation PLDI 2021
Hypercollecting semantics and its application to static analysis of information flow POPL 2017