Constructive Galois Connections

arXiv:1511.06965v4 [] 26 Oct 2016

Taming the Galois Connection Framework for Mechanized Metatheory
David Darais

David Van Horn

University of Maryland, USA
darais@cs.umd.edu

University of Maryland, USA
dvanhorn@cs.umd.edu

Abstract

pings between the domains known as abstraction α ∈ C 7→ A and
concretization γ ∈ A 7→ C such that c ⊑ γ(a) ⇐⇒ α(c)  a.
Since its introduction by Cousot and Cousot in the late 1970s,
this theory has formed the basis of many static analyzers, type
systems, model-checkers, obfuscators, program transformations,
and many more applications [7].
Given the remarkable set of intellectual tools contributed by
this theory, an obvious desire is to incorporate its use into proof
assistants to mechanically verify proofs by abstract interpretation.
When embedded in a proof assistant, verified algorithms such as
static analyzers can then be extracted from these proofs.
Monniaux first achieved the goal of mechanization for the theory of abstract interpretation with Galois connections in Coq [26].
However, he notes that the abstraction side (α) of Galois connections poses a serious problem since it requires the admission of
non-constructive axioms. Use of these axioms prevents the extraction of certified programs. So while Monniaux was able to mechanically verify proofs by abstract interpretation in its full generality,
certified artifacts could not generally be extracted.
Pichardie subsequently tackled the extraction problem by mechanizing a restricted formulation of abstract interpretation that relied
only on the concretization (γ) side of Galois connections [29]. Doing so avoids the use of axioms and enables extraction of certified
artifacts. This proof technique is effective and has been used to construct several certified static analyzers [1, 5, 6, 29], most notably the
Verasco static analyzer, part of the CompCert C compiler [18, 19].
Unfortunately, this approach sacrifices the full generality of the theory. While in principle the technique could achieve mechanization
of existing soundness theorems, it cannot do so faithful to existing
proofs. In particular, Pichardie writes [29, p. 55]:1

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
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 connection 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: one uses calculational
abstract interpretation to design a static analyzer, the other 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.
Categories and Subject Descriptors F.3.2 [Semantics of Programming Languages]: Program analysis
Keywords

The framework we have retained nevertheless loses an important property of the standard framework: being able to
derive a correct approximation f ♯ from the specification
α ◦ f ◦ γ. Several examples of such derivations are given
by Cousot [8]. It seems interesting to find a framework for
this kind of symbolic manipulation, while remaining easily
formalizable in Coq.

Abstract Interpretation, Galois Connections, Monads

1. Introduction
Abstract interpretation is a general theory of sound approximation
widely applied in programming language semantics, formal verification, and static analysis [10–14]. In abstract interpretation, properties of programs are related between a pair of partially ordered
sets: a concrete domain, hC, ⊑i, and an abstract domain, hA, i.
When concrete properties have a -most precise abstraction, the
correspondence is a Galois connection, formed by a pair of map-

This important property is the so-called “calculational” style,
whereby an abstract interpreter (f ♯ ) is derived in a correct-byconstruction manner from a concrete interpreter (f ) composed with
abstraction and concretization (α◦f ◦γ). This style of abstract interpretation is detailed in Cousot’s monograph [8], which concludes:

Permission to make digital or hard copies of all or part of this work for personal or
classroom use is granted without fee provided that copies are not made or distributed
for profit or commercial advantage and that copies bear this notice and the full citation
on the first page. Copyrights for components of this work owned by others than ACM
must be honored. Abstracting with credit is permitted. To copy otherwise, or republish,
to post on servers or to redistribute to lists, requires prior specific permission and/or a
fee. Request permissions from Permissions@acm.org.
Copyright is held by the owner/author(s). Publication rights licensed to ACM.
ICFP’16, September 18–24, 2016, Nara, Japan
ACM. 978-1-4503-4219-3/16/09...$15.00
http://dx.doi.org/10.1145/2951913.2951934

The emphasis in these notes has been on the correctness of
the design by calculus. The mechanized verification of this
formal development using a proof assistant can be foreseen
with automatic extraction of a correct program from its
correctness proof.
1

1

Translated from French by the present authors.

2. Verifying a Simple Static Analyzer

In the subsequent 17 years, this vision has remained unrealized,
and clearly the paramount technical challenge in achieving it is
obtaining both generality and constructivity in a single framework.
This paper contributes constructive Galois connections, a framework for mechanized abstract interpretation with Galois connections that achieves both generality and constructivity, thereby enabling calculational style proofs which make use of both abstraction (α) and concretization (γ), while also maintaining the ability
to extract certified static analyzers.
We develop constructive Galois connections from the insight
that many classical Galois connections used in practice are of a particular restricted form, which is reminiscent of a direct-style verification. Constructive Galois connections are the general abstraction
theory for this setting and can be mechanized effectively.
We observe that constructive Galois connections contain monadic
structure which isolates classical specifications from constructive
algorithms. Within the effectful fragment, all of classical Galois
connection reasoning can be employed, while within the pure fragment, functions must carry computational content. Remarkably,
calculations can move between these modalities and verified programs may be extracted from the end result of calculation.
To support the utility of our theory we build a library for constructive Galois connections in Agda [28] and mechanize two existing abstract interpretation proofs from the literature. The first is
drawn from Cousot’s monograph [8], which derives a correct-byconstruction analyzer from a specification induced by a concrete
interpreter and Galois connection. The second is drawn from Garcia, Clark and Tanter’s “Abstracting Gradual Typing” [17], which
uses abstract interpretation to derive static and dynamic semantics for gradually typed languages from traditional static types.
Both proofs use the “important property of the standard framework” identified by Pichardie, which is not handled by prior mechanization approaches. The mechanized proofs closely follow the
original pencil-and-paper proofs, which use both abstraction and
concretization, while still enabling the extraction of certified algorithms. Neither of these papers have been previously mechanized.
Moreover, we know of no existing mechanized proof involving calculational abstract interpretation.
Finally, we develop the metatheory of constructive Galois connections, prove them sound, and make precise their relationship
to classical Galois connections. The metatheory is itself mechanized; claims are marked with “AGDAX” whenever they are proved
in Agda. (All claims are marked.)

In this section we contrast two perspectives on verifying a static analyzer: using a direct approach, and using the theory of abstract interpretation with Galois connections. The direct approach is simple
but lacks the benefits of a general abstraction framework. Abstract
interpretation provides these benefits, but at the cost of added complexity and resistance to mechanized verification. In Section 3 we
present an alternative perspective: abstract interpretation with constructive Galois connections—the topic of this paper. Constructive
Galois connections marry the worlds presented in this section, providing the simplicity of direct verification, the benefits of a general
abstraction framework, and support for mechanized verification.
To demonstrate both verification perspectives we design a parity
analyzer in each style. For example, a parity analysis discovers
that 2 has parity even, succ(1) has parity even, and n + n has
parity even if n has parity odd. Rather than sketch the highlevel details of a complete static analyzer, we instead zoom into
the low-level details of a tiny fragment: analyzing the successor
arithmetic operation succ(n). At this level of detail the differences,
advantages and disadvantages of each approach become apparent.
2.1 The Direct Approach
Using the direct approach to verification one designs the analyzer,
defines what it means for the analyzer to be sound, and then completes a proof of soundness. Each step is done from scratch, and in
the simplest way possible.
This approach should be familiar to most readers, and exemplifies how most researchers approach formalizing soundness for
static analyzers: first posit the analyzer and soundness framework,
then attempt the proof of soundness. One limitation of this approach is that the setup—which gives lots of room for error—isn’t
known to be correct until after completing the final proof. However,
a benefit of this approach is it can easily be mechanized.
Analyzing Successor A parity analysis answers questions like:
“what is the parity of succ(n), given that n is even?” To answer
these questions, imagine replacing n with the symbol even, a
stand-in for an arbitrary even number. This hypothetical expression
succ(even) is interpreted by defining a successor function over
parities, rather than numbers, which we call succ♯ . This successor
operation on parities is designed such that if p is the parity for n,
succ♯ (p) will be the parity of succ(n):

Contributions This paper contributes the following:

P := {even, odd}

succ♯ (even) := odd

succ♯ : P → P

succ♯ (odd) := even

Soundness The soundness of succ♯ is defined using an interpretation for parities, which we notate JpK:

• a foundational theory of constructive Galois connections which

is both general and amenable to mechanization using a dependently typed functional programming language;

J K : P → ℘(N)

• a proof library and two case studies from the literature for

JevenK := {n | even(n)}
JoddK := {n | odd(n)}

Given this interpretation, a parity p is a valid analysis result for a
number n if the interpretation for p contains n, that is n ∈ JpK. The
analyzer succ♯ (p) is then sound if, when p is a valid analysis result
for some number n, succ♯ (p) is a valid analysis result for succ(n):

mechanized abstract interpretation; and
• the first mechanization of calculational abstract interpretation.

The remainder of the paper is organized as follows. First we
give a tutorial on verifying a simple analyzer from two different
perspectives: direct verification (§2.1) and abstract interpretation
with Galois connections (§2.2), highlighting mechanization issues
along the way. We then present constructive Galois connections as a
marriage of the two approaches (§3). We provide two case studies:
the mechanization of an abstract interpreter from Cousot’s calculational monograph (§4), and the mechanization of Garcia, Clark and
Tanter’s work on gradual typing via abstract interpretation (§5). Finally, we formalize the metatheory of constructive Galois connections (§6), relate our work to the literature (§7), and conclude (§8).

n ∈ JpK =⇒ succ(n) ∈ Jsucc♯ (p)K

(DA-Snd)

The proof is by case analysis on JpK; we show the case p = even:

2

n ∈ JevenK
⇔ even(n)
⇔ odd(succ(n))
⇔ succ(n) ∈ JoddK

* defn. of J K +
* defn. of even/odd +
* defn. of J K +

⇔ succ(n) ∈ Jsucc♯ (even)K

* defn. of succ♯ +

An Even Simpler Setup There is another way to define and prove
soundness: use a function which computes the parity of a number
in the definition of soundness. This approach is even simpler, and
will help foreshadow the constructive Galois connection setup.
parity : N → P

2.2 Classical Abstract Interpretation
To verify an analyzer using abstract interpretation with Galois connections, one first designs abstraction and concretization mappings
between sets N and P. These mappings are used to synthesize an
optimal specification for succ♯ . One then proves that a postulated
succ♯ meets this synthesized specification, or alternatively derives
the definition of succ♯ directly from the optimal specification.
In contrast to the direct approach, rather than design the definition of soundness, one instead designs the definition of abstraction within a structured framework. Soundness is not designed, it
is derived from the definition of abstraction. Finally, there is added
boilerplate in the abstract interpretation approach, which requires
lifting definitions and proofs to powersets ℘(N) and ℘(P).

parity(0) := even
parity(succ(n)) := f lip(parity(n))

where f lip(even) := odd and f lip(odd) := even. This gives an
alternative and equivalent way to relate a number and a parity, due
to the following correspondence:
n ∈ JpK ⇐⇒ parity(n) = p

(DA-Corr)

The soundness of the analyzer is then restated:
parity(n) = p =⇒ parity(succ(n)) = succ♯ (p)

Abstracting Sets Powersets are introduced in abstraction and
concretization functions to support relational mappings, like mapping the symbol even to the set of all even numbers. The mappings
are therefore between powersets ℘(N) and ℘(P). The abstraction
and concretization mappings must also satisfy correctness criteria,
detailed below, at which point they are called a Galois connection.
The abstraction mapping from ℘(N) to ℘(P) is notated α, and
is defined as the pointwise lifting of parity(n):

or by substituting parity(n) = p:
parity(succ(n)) = succ♯ (parity(n))

(DA-Snd*)

Both this statement for soundness and its proof are simpler than
before. The proof follows directly from the definition of parity
and the fact that succ♯ is identical to f lip.

The concretization mapping from ℘(P) to ℘(N) is notated γ, and
is defined as the flattened pointwise lifting of JpK:
γ(P ) := {n | p ∈ P ∧ n ∈ JpK}

γ : ℘(P) → ℘(N)

The correctness criteria for α and γ is the correspondence:
N ⊆ γ(P ) ⇐⇒ α(N ) ⊆ P

(GC-Corr)

The correspondence means that, to relate elements of different
sets—in this case ℘(N) and ℘(P)—it is equivalent to relate them
through either α or γ. Mappings like α and γ which share this
correspondence are called Galois connections.
An equivalent correspondence to (GC-Corr) is two laws relating
compositions of α and γ, called expansive and reductive:

Mechanized Verification This direct approach to verification is
amenable to mechanization using proof assistants like Coq and
Agda. These tools are founded on constructive logic in part to
support verified program extraction. In constructive logic, functions
f : A → B are computable and often defined inductively to ensure
they can be extracted and executed as programs. Analogously,
propositions P : ℘(A) are encoded constructively as undecidable
predicates P : A → prop where x ∈ P ⇔ P (x).
To mechanize the verification of succ♯ we first translate its
definition to a constructive setting unmodified. Next we translate
JpK to a relation I(p, n) defined inductively on n:
I(even, 0)

α(N ) := {parity(n) | n ∈ N }

α : ℘(N) → ℘(P)

The Main Idea Correspondences like (DA-Corr)—between an
interpretation for analysis results (JpK) and a function which computes analysis results (parity(n))—are central to the constructive
Galois Connection framework we will describe in Section 3. Using
correspondences like these, we build a general theory of abstraction
that recovers this direct approach to verification, mirrors all of the
benefits of abstract interpretation with classical Galois connections,
supports mechanized verification, and in some cases simplifies the
proof effort. We also observe that many classical Galois connections used in practice can be ported to this simpler setting.

N ⊆ γ(α(N ))
α(γ(P )) ⊆ P

(GC-Exp)
(GC-Red)

Property (GC-Red) ensures α is the best abstraction possible w.r.t.
γ. For example, a hypothetical definition α(N ) := {even, odd} is
expansive but not reductive because α(γ({even})) 6⊆ {even}.
In general, Galois connections are defined for arbitrary posets
hA, ⊑A i and hB, ⊑B i. The correspondence (GC-Corr) and its expansive/reductive variants are generalized in this setting to use partial orders ⊑A and ⊑B instead of subset ordering. We are also omitting monotonicity requirements for α and γ in our presentation (although (GC-Corr) implies monotonicity).

I(p, n)
I(f lip(p), succ(n))

The mechanized proof of (DA-Snd) using I is analogous to the
one we sketched, and the mechanized proof of (DA-Snd*) follows
directly by computation. The proof term for (DA-Snd*) in both Coq
and Agda is simply refl, the reflexivity judgment for syntactic
equality modulo computation in constructive logic.

Powerset Lifting The original functions succ and succ♯ cannot
be related through α and γ because they are not functions between
powersets. To remedy this they are lifted pointwise:

Wrapping Up The two different approaches to verification we
present are distinguished by which parts of the design are postulated, and which parts are derived. Using the direct approach, the
analysis succ♯ , the interpretation for parities JpK and the definition
of soundness are all postulated up-front. When the soundness setup
is correct but the analyzer is wrong, the proof at the end will not go
through and the analyzer must be redesigned. Even worse, when the
soundness setup and the analyzer are both wrong, the proof might
actually succeed, giving a false assurance in the soundness of the
analyzer. However, the direct approach is attractive because it is
simple and supports mechanized verification.

↑succ : ℘(N) → ℘(N)

↑succ(N ) := {succ(n) | n ∈ N }

↑succ♯ : ℘(P) → ℘(P)

↑succ♯ (P ) := {succ♯ (p) | p ∈ P }

These lifted operations are called the concrete interpreter and abstract interpreter, because the former operates over the concrete
domain ℘(Z) and the latter over the abstract domain ℘(P). In
the framework of abstract interpretation, static analyzers are just
abstract interpreters. Lifting to powersets is necessary to use the
abstract interpretation framework, and has the negative effect of
adding boilerplate to definitions and proofs of soundness.

3

Soundness The definition of soundness for succ♯ is synthesized
by relating ↑succ♯ to ↑succ composed with α and γ:
α(↑succ(γ(P ))) ⊆ ↑succ♯ (P )

Calculational Derivation of Abstract Interpreters Rather than
posit ↑succ♯ and prove it correct directly, one can instead derive its
definition through a calculational process. The process begins with
the optimal specification on the left-hand-side of (GC-Opt), and
reasons equationally towards the definition of a function. In this
way, ↑succ♯ is not postulated, rather it is derived by calculation,
and the result is both sound and optimal by construction.
The derivation is by case analysis on P which has four cases:
{}, {even}, {odd} and {even, odd}; we show P = {even}:

(GC-Snd)

The left-hand side of the ordering is an optimal specification for any
abstraction of ↑succ (a consequence of (GC-Corr)), and the subset ordering says ↑succ♯ is an over-approximation of this optimal
specification. The reason to over-approximate is because the specification is a mathematical description, and the abstract interpreter
is usually an algorithm, and therefore not always able to match the
specification precisely. The proof of (GC-Snd) is by case analysis
on P . We do not show the proof, rather we demonstrate a proof
later in this section which also synthesizes the definition of succ♯ .
One advantage of the abstract interpretation framework is that it
gives the researcher the choice between four soundness properties,
all of which are equivalent and generated by α and γ:
♯

α(↑succ(γ(P ))) ⊆ ↑succ (P )

(GC-Snd/αγ)

↑succ(γ(P )) ⊆ γ(↑succ♯ (P ))

(GC-Snd/γγ)

♯

α(↑succ(N )) ⊆ ↑succ (α(N ))
♯

↑succ(N ) ⊆ γ(↑succ (α(N )))

(GC-Snd/αα)
(GC-Snd/γα)

(GC-Opt)

Not all analyzers are optimal, however optimality helps identify
those which approximate too much. Consider the analyzer ↑succ♯′ :
↑succ♯′ (P ) := {even, odd}

Resistance to Mechanized Verification Despite the beauty and
utility of Galois connections, advocates of the approach have yet to
reconcile their use with advances in mechanized reasoning: every
mechanized verification of an executable abstract interpreter todate has resisted the use of Galois connections, even when initially
designed to take advantage of the framework.
The issue in mechanizing Galois connections amounts to a conflict between supporting both classical set-theoretic reasoning and
executable static analyzers. Supporting executable static analyzers
calls for constructive mathematics, a problem for α functions because they are often non-constructive, an observation first made
by Monniaux [26]. To work around this limitation, Pichardie [29]
advocates for designing abstract interpreters which are merely inspired by Galois connections, but ultimately avoiding their use
in verification, which he terms the “γ-only” approach. Successful verification projects such as Verasco adopt this “γ-only” approach [18, 19], despite the use of Galois connections in designing
the original Astrée analyzer [4].
To better understand the foundational issues with Galois connections and α functions, consider verifying the abstract interpretation approach to soundness for our parity analyzer using a
proof assistant built on constructive logic. In this setting, the encoding of the Galois connection must support elements of infi-

This analyzer reports that succ(n) could have any parity regardless
of the parity for n; it’s the analyzer that always says “I don’t know”.
This analyzer is perfectly sound but non-optimal.
Just like soundness, four completeness statements are generated
by α and γ, however each of the statements are not equivalent:
(GC-Cmp/αγ)

↑succ(γ(P )) = γ(↑succ (P ))

(GC-Cmp/γγ)

α(↑succ(N )) = ↑succ♯ (α(N ))

(GC-Cmp/αα)

↑succ(N ) = γ(↑succ♯ (α(N )))

(GC-Cmp/γα)

* defining ↑succ♯ +

Added Complexity The abstract interpretation approach requires
a Galois connection up-front which necessitates the introduction of
powersets ℘(N) and ℘(P). This results in powerset-lifted definitions and adds boilerplate set-theoretic reasoning to the proofs.
This is in contrast to the direct approach which never mentions
powersets of parities. Not using powersets results in more understandable soundness criteria, requires no boilerplate set-theoretic
reasoning, and results in fewer cases for the proof of soundness.
This boilerplate becomes magnified in a mechanized setting where
all details must be spelled out to a proof assistant. Furthermore,
the simpler proof of (DA-Snd*)—which was immediate from the
definition of parity—cannot be recovered within the abstract interpretation framework, which shows one abandons simpler proof
techniques in exchange for the benefits of abstract interpretation.

Because the left-hand-side is an optimal specification, an abstract
interpreter will never be strictly more precise. Therefore, optimality
is written equivalently using an equality:

♯

* defn. of α +

The derivation of the other cases is analogous, and together they
define the implementation of ↑succ♯ .
Deriving analyzers by calculus is attractive because it is systematic, and because it prevents the issue where an analyzer is postulated and discovered to be unsound only after failing to complete
its soundness proof. However, this calculational style of abstract
interpretation is not amenable to mechanized verification with program extraction because α is often non-constructive, an issue we
describe later in this section.

α(↑succ(γ(P ))) ⊇ ↑succ♯ (P )

α(↑succ(γ(P ))) = ↑succ♯ (P )

= {odd}
, ↑succ ({even})

Completeness The mappings α and γ also synthesize an optimality statement for ↑succ♯ , a kind of completeness property, by stating that it under-approximates the optimal specification:

↑succ♯′ : ℘(P) → ℘(P)

* defn. of γ +
* defn. of ↑succ +
* defn. of even/odd +

♯

Because each soundness property is equivalent (also a consequence
of (GC-Corr)), one can choose whichever variant is easiest to prove.
The soundness setup (GC-Snd) is the αγ rule, however any of the
other rules can also be used. For example, one could choose αα
or γα; in these cases the proof considers four disjoint cases for N :
N is empty, N contains only even numbers, N contains only odd
numbers, and N contains both even and odd numbers.

α(↑succ(γ(P ))) = ↑succ♯ (P )

α(↑succ(γ({even})))
= α(↑succ({n | even(n)}))
= α({succ(n) | even(n)})
= α({n | odd(n)})

Abstract interpreters which satisfy the αγ variant are called optimal
because they lose no more information than necessary, and those
which satisfy the γα variant are called precise because they lose no
information at all. The abstract interpreter succ♯ is optimal but not
precise, because γ(↑succ♯ (α({1}))) 6= ↑succ({1})
To overcome mechanization issues with Galois connections, the
state-of-the-art is restricted to use γγ rules only for soundness
(GC-Snd/γγ) and completeness (GC-Cmp/γγ). This is unfortunate
for completeness properties because each completeness variant is
not equivalent.

4

nite powersets—like the set of all even numbers—as well as executable abstract interpreters which manipulate elements of finite
powersets—like {even, odd}. To support representing infinite sets,
the powerset ℘(N) is modelled constructively as a predicate N →
prop. To support defining executable analyzers that manipulate sets
of parities, the powerset ℘(P) is modelled as an enumeration of its
inhabitants, which we call Pc :

Abstracting Sets A constructive Galois connection between sets
A and B contains two mappings: the first is called extraction,
notated η, and the second is called interpretation, notated µ:
η:A→B

η and µ are analogous to classical Galois connection mappings α
and γ. In the parity analysis described in Section 2.1, the extraction
function was parity and the interpretation function was J K.
Constructive Galois connection mappings η and µ must form a
correspondence similar to (GC-Corr):

Pc := {even, odd, ⊥, ⊤}
where ⊥ and ⊤ represent {} and {even, odd}. This enables a
definition for ↑succ♯ : Pc → Pc which can be extracted and
executed. The consequence of this design is a Galois connection
between N → prop and Pc ; the issue is now α:
α : (N → prop) → P

µ : B → ℘(A)

x ∈ µ(y) ⇐⇒ η(x) = y

(CGC-Corr)

The intuition behind the correspondence is the same as before: to
compare an element x in A to an element y in B, it is equivalent to
compare them through either η or µ.
Like classical Galois connections, the correspondence between
η and µ is stated equivalently through two composition laws. Extraction functions η which form a constructive Galois connection
are also a “best abstraction”, analogously to α in the classical setup:

c

This version of α cannot be defined constructively, as doing so
requires deciding predicates over φ : N → prop. To define α one
must perform case analysis on predicates like ∃n, φ(n) ∧ even(n)
to compute an element of Pc , which is not possible for arbitrary φ.
However, γ can be defined constructively:

sound : x ∈ µ(η(x))
tight : x ∈ µ(y) =⇒ η(x) = y

γ : Pc → (N → prop)

(CGC-Ext)
(CGC-Red)

In general, any theorem of soundness using Galois connections
can be rewritten to use only γ, making use of (GC-Corr); this is
the essence of the “γ-only” approach, embodied by the soundness
variant (GC-Snd/γγ). However, this principle does not apply to all
proofs of soundness using Galois connections, many of which mention α in practice. For example, the γ-only setup does not support
calculation in the style advocated by Cousot [8]. Furthermore, not
all completeness theorems can be translated to γ-only style, such as
(GC-Cmp/γα) which is used to show an abstract interpreter is fully
precise.

Aside We use the term extraction function and notation η from
Nielson et al [27] where η is used to simplify the definition of an
abstraction function α. We recover α functions from η in a similar
way. However, their treatment of η is a side-note to simplifying
the definition of α and nothing more. We take this simple idea
much further to realize an entire theory of abstraction around η/µ
functions and their correspondences. In this “lowered” theory of
η/µ we describe soundness/optimality criteria and calculational
derivations analogous to that of α/γ while support mechanized
verification, none of which is true of Nielson et al’s use of η.

Wrapping Up Abstract interpretation differs from the direct approach in which parts of the design are postulated and which parts
are derived. The direct approach requires postulating the analyzer
and definition of soundness. Using abstract interpretation, a Galois
connection between sets is postulated instead, and definitions for
soundness and completeness are synthesized from the Galois connection. Also, abstract interpretation support deriving the definition
of a static analyzer directly from its proof of correctness.
The downside of abstract interpretation is that it requires lifting succ and succ♯ into powersets, which results in boilerplate
set-theoretic reasoning in the proof of soundness. Finally, due to
foundational issues, the abstract interpretation framework is not
amenable to mechanized verification while also supporting program extraction using constructive logic.

Induced Specifications Four equivalent soundness criteria are
generated by η and µ just like in the classical framework. Each
soundness statement uses η and µ in a different but equivalent way
(assuming (CGC-Corr)). For a concrete f : A → A and abstract
f ♯ : B → B, f ♯ is sound if f any of the following properties hold:
x ∈ µ(y) ∧ y ′ = η(f (x)) =⇒ y ′ = f ♯ (y)
′

′

♯

x ∈ µ(y) ∧ x = f (x) =⇒ x ∈ µ(f (y))
♯

(CGC-Snd/ηµ)
(CGC-Snd/µµ)

y = η(f (x)) =⇒ y = f (η(x))

(CGC-Snd/ηη)

x′ = f (x) =⇒ x′ ∈ µ(f ♯ (η(x)))

(CGC-Snd/µη)

In the direct approach to verifying an example parity analysis
described in Section 2.1, the first soundness property (DA-Snd) is
generated by the µµ variant, and the second soundness property
(DA-Snd*) which enjoyed a simpler proof is generated by the ηη
variant. We write these soundness rules in a slightly strange way
so we can write their completeness analogs simply by replacing
⇒ with ⇔. The origin of these rules comes from an adjunction
framework, which we discuss in Section 6.
The mappings η and µ also generate four completeness criteria
which, like classical Galois connections, are not equivalent:

3. Constructive Galois Connections
In this section we describe abstract interpretation with constructive Galois connections—a parallel universe of Galois connections
analogous to classical ones. The framework enjoys all the benefits
of abstract interpretation, but like the direct approach avoids the
pitfalls of added complexity and resistance to mechanization.
We will describe the framework of constructive Galois connections between sets A and B. When instantiated to N and P, the
framework recovers exactly the direct approach from Section 2.1.
We will also describe constructive Galois connections in the absence of partial orders, or more specifically, we will assume the
discrete partial order: x ⊑ y ⇔ x = y. (Partial orders didn’t appear in our demonstration of classical abstract interpretation, but
they are essential to the general theory.) We describe generalizing
to partial orders and recovering classical results from constructive
ones at the end of this section. The fully general theory of constructive Galois connections is described in Section 6 where it is
compared side-by-side to classical Galois connections.

x ∈ µ(y) ∧ y ′ = η(f (x)) ⇐⇒ y ′ = f ♯ (y)
′

′

(CGC-Cmp/ηµ)

♯

x ∈ µ(y) ∧ x = f (x) ⇐⇒ x ∈ µ(f (y)) (CGC-Cmp/µµ)
y = η(f (x)) ⇐⇒ y = f ♯ (η(x))
′

′

♯

x = f (x) ⇐⇒ x ∈ µ(f (η(x)))

(CGC-Cmp/ηη)
(CGC-Cmp/µη)

Inspired by classical Galois connections, we call abstract interpreters f ♯ which satisfy the ηµ variant optimal and those which
satisfy the µη variant precise.
The above soundness and completeness rules are stated for concrete and abstraction functions f : A → A and f ♯ : B → B.

5

However, they generalize easily to relations R : ℘(A × A) and
predicate transformers F : ℘(A) → ℘(A) (i.e. collecting semantics) through the adjunction framework discussed in Section 6. The
case studies in Sections 4 and 5 describe abstract interpreters over
concrete relations and their soundness conditions.

and sound and optimal by construction. In addition to these benefits of a general abstraction framework, constructive Galois connections are amenable to mechanized verification. Both extraction
(η) and interpretation (µ) can be mechanized effectively, as well as
proofs of soundness, completeness, and calculational derivations.

Calculational Derivation of Abstract Interpreters The constructive Galois connection framework also supports deriving abstract
interpreters through calculation, analogously to the calculation we
demonstrated in Section 2.2. To support calculational reasoning,
the four logical soundness criteria are rewritten into statements
about subsumption between powerset elements:

3.1 Partial Orders and Monotonicity

♯

{η(f (x)) | x ∈ µ(y)} ⊆ {f (y)}

The full theory of constructive Galois connections generalizes to
posets hA, ⊑iA and hB, ⊑B i by making the following changes:
• Powersets must be downward-closed, that is for X : ℘(A):

x ∈ X ∧ x′ ⊑ x =⇒ x′ ∈ X

(CGC-Snd/ηµ*)

♯

{f (x) | x ∈ µ(y)} ⊆ µ(f (y))

Singleton sets {x} are reinterpreted to mean {x | x′ ⊑ x}.
For mechanization, this means ℘(A) is encoded as an antitonic
function, notated with a down-right arrow A → prop, where
the partial ordering on prop is by implication.

(CGC-Snd/µµ*)

♯

{η(f (x))} ⊆ {f (η(x))}

(CGC-Snd/ηη*)

♯

{f (x)} ⊆ µ(f (η(x)))

(PowerMon)
′

(CGC-Snd/µη*)

• Functions must be monotonic, that is for f : A → A:

x ⊑ x′ =⇒ f (x) ⊑ f (x′ )

The completeness analog to the four rules replaces set subsumption
with equality. Using the ηµ* completeness rule, one calculates
towards a definition for f ♯ starting from the left-hand-side, which
is the optimal specification for abstract interpreters of f .
To demonstrate calculation using constructive Galois connections, we show the derivation of succ♯ from its induced specification, the result of which is sound and optimal (because each step is
= in addition to ⊆) by construction; we show p = even:

(FunMon)

We notate monotonic functions f : A → A. Monotonicity
is required for mappings η and µ, and concrete and abstract
interpreters f and f ♯ .
• The constructive Galois connection correspondence is general-

ized to partial orders in place of equality, that is for η and µ:
x ∈ µ(y) ⇐⇒ η(x) ⊑ y

(CGP-Corr)

{parity(succ(n)) | n ∈ JevenK}
= {parity(succ(n)) | even(n)}
= {f lip(parity(n)) | even(n)}
= {f lip(even)}

* defn. of J K +
* defn. of parity +
* Eq. DA-Corr +

= {odd}

* defn. of f lip +

x ∈ µ(y) ∧ y ′ ⊑ η(f (x)) =⇒ y ′ ⊑ f ♯ (y) (CGP-Snd/ηµ)

, {succ♯ (even)}

* defining succ♯ +

x ∈ µ(y) ∧ x′ ⊑ f (x) =⇒ x′ ∈ µ(f ♯ (y)) (CGP-Snd/µµ)

or alternatively, by generalizing the reductive property:
x ∈ µ(y) =⇒ η(x) ⊑ y

• Soundness criteria are also generalized to partial orders:

y ⊑ η(f (x)) =⇒ y ⊑ f ♯ (η(x))

We will show another perspective on this calculation later in this
section, where the derivation of succ♯ is not only sound and optimal
by construction, but computable by construction as well.

′

′

♯

x ⊑ f (x) =⇒ x ∈ µ(f (η(x)))

(CGP-Snd/ηη)
(CGP-Snd/µη)

We were careful to write the equalities in Section 3 in the right
order so this change is just swappping = for ⊑. Completeness
criteria are identical with ⇔ in place of ⇒.

Mechanized Verification In addition to the benefits of a general abstraction framework, constructive Galois connections are
amenable to mechanization in a way that classical Galois connections are not. In our Agda library and case studies we mechanize
constructive Galois connections in full generality, as well as proofs
that use both mapping functions, such as calculational derivations.
As we discussed in Sections 2.1 and 2.2, the constructive encoding for infinite powersets ℘(A) is A → prop. This results in
the following types for η and µ when encoded constructively:
η:N→P

(CGP-Red)

To demonstrate when partial orders and monotonicity are necessary, consider designing a parity analyzer for the max operator:
max♯ : P × P → P
max♯ (even, even) := even

max♯ (even, odd) := ?

max♯ (odd, odd) := odd

max♯ (odd, even) := ?

The last two cases for max♯ cannot be defined because the maximum of an even and odd number could be either even or odd, and
there is no representative for “any number” in P. To remedy this,
we add any to the set of parities: P+ := P∪{any}; the new element
any is interpreted: JanyK := {n | n ∈ N}; the partial order on P+
becomes: even, odd ⊑ any; and the correspondence continues to
hold using this partial order: n ∈ Jp+ K ⇐⇒ parity(n) ⊑ p+ .
max♯ is then defined using the abstraction P+ and proven sound
and optimal following the abstract interpretation paradigm.

µ : P → N → prop

In constructive logic, the arrow type N → P classifies computable
functions, and the arrow type P → N → prop classifies undecidable relations. (CGC-Corr) is then mechanized without issue:
µ(p, n) ⇐⇒ η(n) = p
See the mechanization details in Section 2.1 for how η and µ are
defined constructively for the example parity analysis.
Wrapping Up Constructive Galois connections are a general abstraction framework similar to classical Galois connections. At the
heart of the constructive Galois connection framework is a correspondence (CGC-Corr) analogous to its classical counterpart. From
this correspondence, soundness and completeness criteria are synthesized for abstract interpreters. Constructive Galois connections
also support calculational derivations of abstract interpreters which

3.2 Relationship to Classical Galois Connections
We clarify the relationship between constructive and classical Galois connections in three ways:
• Any constructive Galois connection can be lifted to obtain an

equivalent classical Galois connection, and likewise for soundness and completeness proofs.

6

• Any classical Galois connection which can be recovered by a

The monadic structure of classical powersets is standard, and is
analogous to the nondeterminism monad familiar to Haskell programmers. However, the model ℘(A) = A → prop is the uncomputable nondeterminism monad and mirrors the use of setcomprehensions on paper to describe uncomputable sets (specifications), rather than the use of monad comprehensions in Haskell
to describe computable sets (constructed values).
We generalize ℘( ) to a monotonic monad, similarly to how
we generalized powersets to posets in Section 3.1. This results in
monotonic versions of monad operators ret and bind:

constructive one contains no additional expressive power, rendering it an equivalent theory with added boilerplate reasoning.
• Not all classical Galois connections can be recovered by con-

structive ones.
From these relationships we conclude that one benefits from using
constructive Galois connections whenever possible, classical Galois connections when no constructive one exists, and both theories
together as needed. We make these claims precise in Section 6.
A classical Galois connection is recovered from a constructive
one by the following lifting:
α : ℘(A) → ℘(B)
γ : ℘(B) → ℘(A)

ret : A → ℘(A)
ret(x) := {x′ | x′ ⊑ x}

α(X) := {η(x) | x ∈ X}
γ(Y ) := {x | y ∈ Y ∧ x ∈ µ(y)}

bind : ℘(A) × (A → ℘(B)) → ℘(B)
bind(X, f ) := {y | x ∈ X ∧ y ∈ f (x)}

We adopt Moggi’s notation [25] for monadic extension where
bind(X, f ) is written f ∗ (X), or just f ∗ for λX.f ∗ (X).
We call the powerset type ℘(A) a specification effect because it
has monadic structure, supports encoding arbitrary properties over
values in A, and cannot be “escaped from” in constructive logic,
similar to the IO monad in Haskell. In classical mathematics, there
is an isomorphism between singleton powersets ℘1 (A) and the set
A. However, no such constructive mapping exists for ℘1 (A) → A.
Such a function would decide arbitrary predicates in A → prop to
compute the A inside the singleton set. This observation, that you
can program inside ℘( ) monadically in constructive logic, but you
can’t escape the monad, is why we call it a specification effect.
Given the monadic structure for powersets, and the intuition
that they encode a specification effect in constructive logic, we can
recast the theory of constructive Galois connections using monadic
operators. To do this we define a helper operator which injects
“pure” functions into the “effectful” function space:

When a classical Galois connection can be written in this form for
some η and µ, then one can use the simpler setting of abstract interpretation with constructive Galois connections without any loss
of generality. We also observe that many classical Galois connections in practice can be written in this form, and therefore can be
mechanized effectively using constructive Galois connections. The
case studies in presented in Sections 4 and 5 are two such cases,
although the original authors of those works did not initially write
their classical Galois connections in this explicitly lifted form.
An example of a classical Galois connection which is not recovered by lifting a constructive Galois is the Independent Attributes
(IA) abstraction, which abstracts relations R : ℘(A × B) with their
component-wise splitting hRl , Rr i : ℘(A) × ℘(B):
α : ℘(A × B) → ℘(A) × ℘(B)
α(R) := h{x | ∃y.hx, yi ∈ R}, {y | ∃x.hx, yi ∈ R}i
γ : ℘(A) × ℘(B) → ℘(A × B)
γ(Rl , Rr ) := {hx, yi | x ∈ Rl , y ∈ Rr }

pure : (A → B) → (A → ℘(B)) pure(f )(x) := ret(f (x))
We then rewrite (CGC-Corr) using ret and pure:
ret(x) ⊆ µ(y) ⇐⇒ pure(η)(x) ⊆ ret(y)

This Galois connection is amenable to mechanized verification. In
a constructive setting, α and γ are maps between A × B → prop
and (A → prop) × (B → prop), and can be defined directly using
logical connectives ∃ and ∧:

(CGM-Corr)

and we rewrite the expansive and reductive variant of the correspondence using ret, bind (notated f ∗ ) and pure:
ret(x) ⊆ µ∗ (pure(η)(x))

α(R) := hλ(x).∃(y).R(x, y), λ(y).∃(x).R(x, y)i
γ(Rl , Rr ) := λ(x, y).Rl (x) ∧ Rr (y)

∗

pure(η) (µ(y)) ⊆ ret(y)

(CGM-Exp)
(CGM-Red)

The four soundness and completeness conditions can also be written in monadic style; we show the ηµ soundness property here:

IA can be mechanized effectively because the Galois connection
consists of mappings between specifications and the foundational
issue of constructing values from specifications does not appear.
IA is not a constructive Galois connection because there is no pure
function µ underlying the abstraction function α.
Because constructive Galois connections can be lifted to classical ones, a constructive Galois connection can interact directly with
IA through its lifting, even in a mechanized setting. However, once
a constructive Galois connection is lifted it loses its computational
properties and cannot be extracted and executed. In practice, IA is
used to weaken (⊑) an induced optimal specification after which
the calculated interpreter is shown to be optimal (=) up-to-IA. IA
never appears in the final calculated interpreter, so not having a
constructive Galois connection formulation poses no issue.

pure(η)∗ (pure(f )∗ (µ(y))) ⊆ pure(f ♯ )(y)

(CGM-Snd)

The left-hand-side of the ordering is the optimal specification for
f ♯ , just like (CGC-Snd/ηµ) but using monadic operators. The righthand-side of the ordering is f ♯ lifted to the monadic function space.
The constructive calculation of succ♯ we showed earlier in this
section is a calculation of this form. The specification on the left
has type ℘(P), and it has effects, meaning it uses classical reasoning
and can’t be executed. The abstract interpreter on the right also has
type ℘(P), but it has no effects, meaning it can be extracted and
executed. The calculated abstract interpreter is thus not only sound
and optimal by construction, it is computable by construction.
Constructive Galois connections are empowering because they
treat specification like an effect, which optimal specifications ought
to have, and which computable abstract interpreters ought not to
have. Using a monadic effect discipline we support calculations
which start with a specification effect, and where the “effect” is
eliminated through the process of calculation. The monad laws
are crucial in canceling uses of ret with bind to arrive at a final
pure computation. For example, the first step in a derivation for
(CGM-Snd) can immediately simplify using monad laws to:

3.3 The “Specification Effect”
The machinery of constructive Galois connections follow a monadic
effect discipline, where the effect type is the classical powerset
℘( ); we call this a specification effect. First we will describe the
monadic structure of powersets ℘( ) and what we mean by “specification effect”. Then we will recast the theory of constructive
Galois connections in this monadic style, giving insights into why
the theory supports mechanized verification, and foreshadowing
key fragments of the metatheory we develop in Section 6.

pure(η ◦ f )∗ (µ(y)) ⊆ pure(f ♯ )(y)

7

i∈
b∈

Z := {. . . , −1, 0, 1, . . .}
B := {true, f alse}

integers

ρ ∈ env := var ⇀ Z
a

ς ∈ Σ ::= hρ, cei
a

J K ∈ aop → Z × Z ⇀ Z

⊢ ⇓

variables

J Kc ∈ cmp → Z × Z → B

⊢ ⇓b ∈ ℘(env × bexp × B)

⊕ ∈ aop ::= + | − | × | /

arithmetic op.

J Kb ∈ bop → B × B → B

< ∈ cmp ::= < | =

comparison op.

<

booleans

x ∈ var ::= . . .

∈ bop ::= ∨ | ∧

arithmetic exp.

be ∈ bexp ::= b | ae < ae | be

boolean exp.

<

ae ∈ aexp ::= i | x | rand | ae ⊕ ae
be

AR AND

ρ ⊢ ae1 ⇓a i1
ρ ⊢ ae2 ⇓a i2
AO P
a
ρ ⊢ ae1 ⊕ ae2 ⇓ J⊕Ka (i1 , i2 )

ce ∈ cexp ::= skip | ce ; ce | x := ae

ρ ⊢ ae ⇓a i
CA SSIGN
hρ, x := aei 7→c hρ[x ← i], skipi

| if be then ce else ce
| while be do ce

7→c ∈ ℘(Σ × Σ)

ρ ⊢ rand ⇓a i

boolean op.

∈ ℘(env × aexp × Z)

command exp.

ρ ⊢ be ⇓b true
CW HILE -T
hρ, while be do cei 7→c hρ, ce ; while be do cei

Figure 1. Case Study: WHILE abstract syntax

ρ ⊢ be ⇓b f alse
CW HILE -F
hρ, while be do cei 7→c hρ, skipi

4. Case Study: Calculational AI
In this section we apply constructive Galois connections to the Calculational Design of a Generic Abstract Interpreter from Cousot’s
monograph [8]. To our knowledge, we achieve the first mechanically verified abstract interpreter derived by calculus.
The key challenge in mechanizing the interpreter is supporting
both abstraction (α) and concretization (γ) mappings, which are required by the calculational approach. Classical Galois connections
do not support mechanization of the abstraction mapping without
the use of axioms, and the required axioms block computation, preventing the extraction of verified algorithms.
To verify Cousot’s generic abstract interpreter we use constructive Galois connections, which we describe in Section 3 and formalize in Section 6. Using constructive Galois connections we encode extraction (η) and interpretation (µ) mappings as constructive
analogs to α and γ, calculate an abstract interpreter for an imperative programming language which is sound and computable by
construction, and recover the original classical Galois connection
results through a systematic lifting.
First we describe the setup for the analyzer: the abstract syntax, the concrete semantics, and the constructive Galois connections involved. Following the abstract interpretation paradigm with
constructive Galois connections we design abstract interpreters for
denotation functions and semantics relations. We show a fragment
of our Agda mechanization which closely mirrors the pencil-andpaper proof, as well as Cousot’s original derivation.

Figure 2. Case Study: WHILE concrete semantics
4.2 Abstract Semantics with Constructive GCs
Using abstract interpretation with constructive Galois connections,
we design an abstract semantics for WHILE in the following steps:
1. An abstraction for each set Z, B and env.
2. An abstraction for each denotation function J Ka , J Kc and J Kb .
3. An abstraction for each semantics relation ⇓a , ⇓b and 7→c .
Each abstract set forms a constructive Galois connection with its
concrete counterpart. Soundness criteria is synthesized for abstract
functions and relations using constructive Galois connection mappings. Finally, we verify and calculate abstract interpreters from
these specifications which are sound and computable by construction. We describe the details of this process only for integers and
environments (the sets Z and env), arithmetic operators (the denotation function J Ka ), and arithmetic expressions (the semantics
relation ⇓a ). See the Agda development accompanying this paper
for the full mechanization of WHILE.
Abstracting Integers We design a simple sign abstraction for integers, although more powerful abstractions are certainly possible [24]. The final abstract interpreter for WHILE is parameterized
by any abstraction for integers, meaning another abstraction can be
plugged in without added proof effort.
The sign abstraction begins with three representative elements:
neg, zer and pos, representing negative integers, the integer 0, and
positive integers. To support representing integers which could be
negative or 0, negative or positive, or 0 or positive, etc. we design
a set which is complete w.r.t these logical disjunctions:

4.1 Concrete Semantics
The WHILE language is an imperative programming language with
arithmetic expressions, variable assignment and while-loops. We
show the syntax for this language in Figure 1. WHILE syntactically
distinguished arithmetic, boolean and command expressions. rand
is an arithmetic expression which can evaluate to any integer. Syntactic categories ⊕, < and range over arithmetic, comparison and
boolean operators, and are introduced to simplify the presentation.
The WHILE language is taken from Cousot’s monograph [8].
The concrete semantics of WHILE is sketched without full definition in Figure 2. Denotation functions J Ka , J Kc and J Kb give
semantics to arithmetic, conditional and boolean operators. The semantics of compound syntactic expressions are given operationally
with relations ⇓a , ⇓b and 7→c . Relational semantics are given for
arithmetic expressions and commands due to the nondeterminism
of rand and nontermination of while. These semantics serve as
the starting point for designing an abstract interpreter.
<

i♯ ∈ Z♯ := {none, neg, zer, pos, negz, nzer, posz, any}
Z♯ is given meaning through an interpretation function µz , the
analog of a γ from the classical Galois connection framework:
µz : Z♯ → ℘(Z)
µz (none) := {}
µz (neg) := {i | i < 0}
µz (zer) := {0}
µz (pos) := {i | i > 0}

8

µz (negz) := {i | i ≤ 0}
µz (nzer) := {i | i 6= 0}
µz (posz) := {i | i ≥ 0}
µz (any) := {i | i ∈ Z}

The partial ordering on abstract integers coincides with subset
ordering through µz , that is i♯1 ⊑z i♯2 ⇐⇒ µz (i♯1 ) ⊆ µz (i♯2 ):

The specification which encodes soundness and optimality for
J K♯a is generated using the constructive Galois connection for Z:

neg ⊑z negz, nzer

pos ⊑z nzer, posz

♯′
z
a
♯′ ♯′
♯a ♯ ♯
hi1,i2i ∈ µz(i♯1,i♯2) ∧ hi♯′
1 ,i2 i ⊑ η (JaeK (i1,i2)) ⇔ hi1 ,i2 i ⊑ JaeK (i1,i2)

zer ⊑z negz, posz

none ⊑z i♯ ⊑z i♯ ⊑z any

(See (CGC-Cmp/ηµ) in Section 3 for the origin of this equation.)
For J K♯a , we postulate its definition and verify its correctness postfacto using the above property, although we omit the proof details
here. The definition of J K♯a is standard, and returns none in the
case of division by zero. We show only the definition of + here:

To be a constructive Galois connection, µz forms a correspondence
with a best abstraction function η z :


neg if i < 0
η z : Z → Z♯
η z (n) := zer if i = 0

pos if i > 0

J K♯a : aexp → Z♯ × Z♯ → Z♯


pos if pos ⊑z



z
neg if neg ⊑
G
♯a ♯ ♯
J+K (i1 , i2 ) :=
zer if zer ⊑z



zer if pos ⊑z



zer if neg ⊑z

and we prove the constructive Galois connection correspondence:
i ∈ µz (i♯ ) ⇐⇒ η z (i) ⊑z i♯

The Classical Design To contrast with Cousot’s original design
using classical abstract interpretation, the key difference is the abstraction function. The abstraction function using classical Galois
connections is recovered through a lifting of our η z :
G z
αz (I) :=
η (i)
αz : ℘(Z) → Z♯

J Ka℘ ∈ aexp → ℘(Z × Z) → ℘(Z)
JaeKa℘ (II) := {JaeKa (i1 , i2 ) | hi1 , i2 i ∈ II}

Abstraction functions of this form—℘(B) → A, for some concrete set A and abstract set B—are representative of most Galois
connections used in the literature for static analyzers. However,
these abstraction functions are precisely the part of classical Galois
connections which inhibit mechanized verification. The extraction
function η z does not manipulate powersets, does not inhibit mechanized verification, and recovers the original non-constructive αz
through this standard lifting.

and then J K♯a is proven correct w.r.t. this lifting using αz and γ z :
αz (JaeKa℘ (γ z (i♯1 , i♯2 ))) = JaeK♯a (i♯1 , i♯2 )
This property cannot be mechanized without axioms because αz is
non-constructive. Furthermore, the proof involves additional powerset boilerplate reasoning, which is not present in our mechanization of correctness for J K♯a using constructive Galois connections.
The state-of-the art approach of “γ-only” verification would instead
mechanize the γγ variant of correctness:

Abstracting Environments An abstract environment maps variables to abstract integers rather than concrete integers.
ρ♯ ∈ env♯ := var → Z♯

JaeKa℘ (γ z (i♯1 , i♯2 )) = γ z (JaeK♯a (i♯1 , i♯2 ))

r

env is given meaning through an interpretation function µ :

which is similar to our µµ rule:

µr ∈ env♯ → ℘(env) µr (ρ♯ ) := {ρ | ∀x.ρ(x) ∈ µz (ρ♯ (x))}
An abstract environment represents concrete environments that
agree pointwise with some represented integer in the codomain.
The order on abstract environments is the standard pointwise
ordering and obeys ρ♯1 ⊑r ρ♯2 ⇐⇒ µr (ρ♯1 ) ⊆ µr (ρ♯2 ):

hi1, i2i ∈ µz(i♯1,i♯2) ∧ hi′1, i′2i = JaeKa(i1,i2) ⇔ hi′1, i′2i ∈ µz(JaeK♯a(i♯1,i♯2))
The benefit of our approach is that soundness and completeness
properties which also mention extraction (η) can also be mechanized, like calculating abstract interpreters from their specification.
Abstracting Relations The verification of an abstract interpreter
for relations is similar to the design for functions: induce a specification using the constructive Galois connection, and prove correctness w.r.t. the induced spec. The relations we abstract are ⇓a ,
⇓b and 7→c , and we call their abstract interpreters A♯ , B♯ and C ♯ .
Rather than postulate the definitions of the abstract interpreters, we
calculate them from their specifications, the results of which are
sound and computable by construction. The arithmetic and boolean
abstract interpreters are functions from abstract environments to abstract integers, and the abstract interpreter for commands computes
the next abstract transition states of execution. We only present select calculations for A♯ ; see our accompanying Agda development
for each calculation in mechanized form. A♯ has type:

ρ♯1 ⊑r ρ♯2 ⇐⇒ (∀x.ρ♯1 (x) ⊑z ρ♯2 (x))
To form a constructive Galois connection, µr forms a correspondence with a best abstraction function η r :
η r ∈ env → env♯

i♯2
i♯2
i♯2
i♯2
i♯2

The Classical Design To contrast with Cousot’s original design
using classical abstract interpretation, the key difference is that we
avoid powerset liftings all-together. Using classical Galois connections, the concrete denotation function must be lifted to powersets:

i∈I

♯

i♯1 ∨ pos ⊑z
i♯1 ∨ neg ⊑z
i♯1 ∧ zer ⊑z
i♯1 ∧ neg ⊑z
i♯1 ∧ pos ⊑z

η r (ρ) := λx.η z (ρ(x))

and we prove the constructive Galois connection correspondence:
ρ ∈ µr (ρ♯ ) ⇐⇒ η r (ρ) ⊑r ρ♯
The Classical Design To contrast with Cousot’s original design
using classical abstract interpretation, the key difference is again
the abstraction function. The abstraction function using classical
Galois connections is:

A♯ [ ] : aexp → env♯ → Z♯

αr (R) := λx.αz ({ρ(x) | ρ ∈ R})
αr : ℘(env) → env♯
which is also not amenable to mechanized verification.

To induce a spec for A♯ , we first revisit the concrete semantics
relation as a powerset-valued function, which we call A:

Abstracting Functions After designing constructive Galois connections for Z and env we define what it means for J K♯a , some abstract denotation for arithmetic operators, to be a sound abstraction
of J Ka , its concrete counterpart. This is done through a specification induced by mappings η and µ, analogously to how specifications are induced using classical Galois connections.

A[ ] : aexp → env → ℘(Z)

A[ae](ρ) := {i | ρ ⊢ ae ⇓a i}

The induced spec for A♯ is generated with the monadic bind operator, which we notate using Moggi’s star notation ∗ :
pure(η z )∗ (A[ae]∗ (µr (ρ♯ ))) ⊆ pure(A♯ [ae])(ρ♯ )

9

Case ae = rand:
z

r

-- Agda Calculation of Case ae = x:
♯

a

α[A] (Var x) ρ♯ = [proof-mode]

{η (i) | ρ ∈ µ (ρ ) ∧ ρ ⊢ rand ⇓ i}
z

r

♯

do [[ (pure · η z ) ∗ · (A[ Var x ] ∗ · (µr · ρ♯)) ]]

a

= {η (i) | ρ ∈ µ (ρ ) ∧ i ∈ Z}

* defn. of ρ ⊢ rand ⇓ i +

⊆ {η z (i) | i ∈ Z}

* ∅ when µr (ρ♯ ) = ∅ +

⊆ {any}

* {any} mon. w.r.t. ⊑z +

, {A♯ [rand](ρ♯ )}

* defining A♯ [rand] +

 [focus-right [· ] of (pure · η z ) ∗ ] begin
do [[ A[ Var x ] ∗ · (µr · ρ♯) ]]
 * A[Var]/≡ +
 [[ (pure · lookup[ x ]) ∗ · (µr · ρ♯) ]]

Case ae = x:

 * lookup/µr /≡ +

{η z (i) | ρ ∈ µr (ρ♯ ) ∧ ρ ⊢ x ⇓a i}

 [[ µz ∗ · (pure · lookup♯[ x ] · ρ♯) ]]

= {η z (ρ(x)) | ρ ∈ µr (ρ♯ )}

* defn. of ρ ⊢ x ⇓a i +

= {η z (i) | i ∈ µz (ρ♯ (x))}

* defn. of µr (ρ♯ ) +

 [[ (pure · η z ) ∗ · (µz ∗ · (pure · lookup♯[ x ] · ρ♯)) ]]

* Eq. CGC-Red +

 * reductive[ηµ] +

♯

⊆ {ρ (x)}
♯

♯

end

♯

, {A [x](ρ )}

 [[ ret · (lookup♯[ x ] · ρ♯) ]]

* defining A [x] +

 [[ pure · A♯[ Num n ] · ρ♯ ]] 

Case ae = x (Monadic):
z ∗

r

∗

♯

pure(η ) (A[x] (µ (ρ )))

Figure 4. Constructive GC calculations in Agda

= pure(λρ.η z (ρ(x)))∗ (µr (ρ♯ ))

* defn. of A[x] +

= pure(η z )∗ (µz∗ (ρ♯ (x)))

* defn. of µr (ρ♯ ) +

⊆ ret(ρ♯ (x))

* Eq. CGC-Red +

♯

♯

, pure(A [x])(ρ )

The Classical Design Classically, one first designs a powerset
lifting of the concrete semantics, called a collecting semantics:
A℘ [ ] : aexp → ℘(env) → ℘(Z)
A℘ [ae](R) := {i | ρ ∈ R ∧ ρ ⊢ ae ⇓a }

* defining A♯ [x] +

The classical soundness specification for A♯ [ae](ρ♯ ) is then:

Figure 3. Constructive GC calculations on paper

αz (A℘ [ae](γ r (ρ♯ ))) ⊑ A♯ [ae](ρ♯ )
However, as usual, the abstraction αz cannot be mechanized effectively, preventing a mechanized derivation of A♯ by calculus.

which unfolds to:
{η z (i) | ρ ∈ µr (ρ♯ ) ∧ ρ ⊢ ae ⇓a i} ⊆ {A♯ [ae](ρ♯ )}

5. Case Study: Gradual Type Systems

To calculate A♯ we reason equationally from the spec on the left
towards the singleton set on the right, and declare the result the
definition of A♯ . We do this by case analysis on ae; we show the
cases for ae = rand and ae = x in Figure 3. Each calculation can
also be written in monadic form, which is the style we mechanize;
we repeat the variable case in monadic form in the figure.

Recent work in metatheory for gradual type systems by Garcia
et al. [17] shows how a Galois connection discipline can guide the
design of gradual typing systems. Starting with a Galois connection
between precise and gradual types, both the static and dynamic
semantics of the gradual language are derived systematically. This
technique is called Abstracting Gradual Typing (AGT).
The design presented by Garcia et al is to begin with a precise
type system, like the simply typed lambda calculus, and add a new
type ? which functions as the ⊤ element in the lattice of type precision. The precise typing
rules are presented with meta-operators <:
..
for subtyping and ∨ for the join operator in the subtyping lattice.
The gradual type system is then written using abstract variants <:♯
.. ♯
and ∨ which are proven correct w.r.t. specifications induced by the
Galois connection.

Mechanized Calculation Our Agda calculation of A♯ strongly
resembles the on-paper monadic one. We show the Agda proof
code for abstract variable references in Figure 4. The first line is the
top level definition site for the derivation of A♯ for the Var case.
The proof-mode term is part of our “proof-mode” library which
gives support for calculational reasoning in the form of Agda proof
combinators with mixfix syntax. Statements surrounded by double
square brackets [[e]] restate the current proof state, which Agda will
check is correct. Reasoning steps are employed through *e+ terms,
which transform the proof state from the previous form to the next.
The term [focus-right [· ] of e] focuses the goal to the right of
the outermost application, scoped between begin and end.
Using constructive Galois connections, our mechanized calculation closely follows Cousot’s classical one, uses both η and µ
mappings, and results in a verified, executable static analyzer. Such
a result is not possible using classical Galois connections, due to
the inability to encode α functions constructively.
We complete the full calculation of Cousot’s generic abstract
interpreter for WHILE in Agda as supplemental material to this
paper, where the resulting interpreter is both sound and computable
by construction. We also provide our “proof-mode” library which
supports general calculational reasoning with posets.

The Precise Type System The AGT paper describes two designs
for gradual type systems in increasing complexity. We chose to
mechanize a hybrid of the two which is simple, like the first design, yet still exercises key challenges addressed by the second. We
also made slight modifications to the design at parts to make mechanization easier, but without changing the nature of the system.
The precise type system we mechanized is the simply typed
lambda calculus with booleans, and top and bottom elements for
a subtyping lattice, which we call any and none:
τ ∈ type ::= none | B | τ → τ | any
The first design in the AGT paper does not involve subtyping,
and their second design incorporates record types with width and
depth subtyping. By just focusing on none and any, we exercise

10

Γ ⊢ e 1 : τ1
Γ ⊢ e 2 : τ2
Γ ⊢ e 3 : τ3

Γ♯ ⊢♯ e♯1 : τ1♯
Γ♯ ⊢♯ e♯2 : τ2♯
Γ♯ ⊢♯ e♯3 : τ3♯

τ1 <: B
..

Γ ⊢ if e1 then e2 else e3 : τ1 ∨ τ2

IF

.. ♯

Γ♯ ⊢♯ if e1 then e2 else e3 : τ1♯ ∨ τ2♯

Γ ⊢ e 1 : τ1
τ1 <: τ11 → τ21
Γ ⊢ e 2 : τ2
τ2 <: τ11
A PP
Γ ⊢ e1 (e2 ) : τ21

Γ♯ ⊢♯ e♯1 : τ1♯
Γ♯ ⊢♯ e♯2 : τ2♯

Γ♯ ⊢♯ e♯ : τ1♯

closed(un) =⇒ ⊢ ⌈un⌉ : ?
⊢

♯
♯
♯
♯
♯
♯
♯
♯
τ11
⊑ τ12
∧ τ21
⊑ τ22
=⇒ τ11
→ τ21
⊑ τ12
→ τ22

Just as in our other designs by abstract interpretation, type♯ is
given meaning by an interpretation function µ, which is the constructive analog of a classical concretization (γ) function:
µ : type♯ → ℘(type)
µ(?) := {τ | τ ∈ type}
µ(τ1♯ → τ2♯ ) := {τ1 → τ2 | τ1 ∈ µ(τ1♯ ) ∧ τ2 ∈ µ(τ2♯ )}
The extraction function η is, remarkably, the identity function:
η(τ ) = τ

and the constructive Galois correspondence holds:
τ ∈ µ(τ ♯ ) ⇐⇒ η(τ ) ⊑ τ ♯

.. ♯

hτ1 , τ2 i ∈ µ(τ1♯ , τ2♯ ) ∧ τ3♯ ⊑ η(τ1 ∨ τ2 ) ⇐⇒ τ3♯ ⊑ τ1♯ ∨ τ2♯
Key properties of gradual subtyping and the gradual join operator
is how they operate over the unknown type ?:
? <: τ

τ <: ?

⊑

e♯2

=⇒ ⊢

(EDL)
♯

e♯2

:

τ2♯

∧

τ1♯

⊑

τ2♯

(GG)

Kleisli Galois Connections We summarize Kleisli Galois connections in Figure 7. Kleisli Galois connections are analogous to
classical ones, but with monadic analogs to α and γ, and monadic
identity and composition operators ret and ⊛ in place of the function space identity and composition operators id and ◦.

τ1 ∈ µ(τ1♯ ) ∧ τ2 ∈ µ(τ2♯ ) ∧ τ1 <: τ2 ⇐⇒ τ1♯ <:♯ τ2♯

♯

∧

e♯1

Powerset Monad See Sections 3.1 and 3.3 for the downwardclosure monotonicity property, and monad definitions and notation
for the monotonic powerset monad. The monad operators obey
standard monad laws. We introduce one new operator for monadic
function composition: (g ⊛ f )(x) := g ∗ (f (x)).

Gradual Operators Given the constructive Galois connection between gradual and precise types, we synthesize specifications for
..
abstract analogs of subtyping <: and the subtyping join operator ∨,
.. ♯
and relate them to their abstractions <:♯ and ∨ :

.. ♯

:

τ1♯

Classical Galois Connections We review classical Galois connections in Figure 7. A Galois connection between posets A and
B contains two adjoint functors α and γ which share a correspondence. An equivalent formulation of the correspondence is two unit
equations called extensive and reductive. Abstract interpreters are
sound by over-approximating a specification induced by α and γ.

τ ♯ ∈ {none, B, any}

♯

e♯1

In this section we develop the full metatheory of constructive Galois connection and prove precise claims about their relationship to
classical Galois connections. We develop the metatheory of constructive Galois connections as an adjunction between posets with
powerset-Kleisli adjoint functors. This is in contrast to classical Galois connections which come from an identical setup, but with the
monotonic function space as adjoint functors, as shown in Figure 7.
We connect constructive to classical Galois connections through
an isomorphism between a subset of classical to the entire space of
constructive. To form this isomorphism we introduce an intermediate structure, Kleisli Galois connections, which we show are isomorphic to the classical subset, and isomorphic to constructive ones
using the constructive theorem of choice, as depicted in Figure 8.

♯

And arrow types are monotonic:

♯

♯

6. Constructive Galois Connection Metatheory

τ ⊑τ ⊑?

♯

(FAT)

♯

The partial ordering is reflexive and has ? at the top:

♯

G-C OE

⊢ e : τ ⇐⇒ ⊢♯ e : τ

τ ♯ ∈ type♯ ::= none | B | τ ♯ → τ ♯ | any | ?

..

G-A PP

Gradual Metatheory Using AGT, the gradual type system is a
syntactic analog to the precise one but with gradual types and
operators, which we show in Figure 6. Using this system, and
constructive Galois connections, we mechanize in Agda the key
AGT metatheory results from the paper: equivalence for fullyannotated terms (FAT), embedding of dynamic language terms
(EDL), and gradual guarantee (GG):

Gradual Types The essence of AGT is to design a gradual type
system by abstract interpretation of the precise type system. To do
this, a new top element is added to the precise type system, although
rather than representing the top of the subtyping lattice like any, it
represents the top of the precision lattice, and is notated ?:

η : type → type♯

G-I F

Figure 6. Case Study: gradual type system

the subtyping machinery of their approach without the blowup in
complexity from formalizing record types.
The typing rules in AGT are written in strictly syntax-directed
form, with explicit use of subtyping in rule hypotheses. We show
three precise typing rules for if-statements, application and coercion in Figure 5. The subtyping lattice in the precise system is
the “safe for substitution” lattice, and well typed programs enjoy
progress and preservation.

when

τ1♯ <:♯ τ2♯

Γ♯ ⊢♯ e♯ :: τ2♯ : τ2♯

Figure 5. Case Study: precise type system

µ(τ ♯ ) := τ ♯

♯
♯
τ1♯ <:♯ τ11
→ τ21
♯
♯ ♯
τ2 <: τ11

♯
Γ♯ ⊢ e♯1 (e♯2 ) : τ21

Γ ⊢ e : τ1
τ1 <: τ2
C OE
Γ ⊢ e :: τ2 : τ2

♯

τ1♯ <:♯ B

Kleisli to Classical and Back All Kleisli Galois connections
hκα, κγi between A and B can be lifted to recover a classical Galois connection hα, γi between ℘(A) and ℘(B) through a monadic

♯ .. ♯

?∨ τ =τ ∨ ?=?

11

Adjunction
Category
Adjoints
LAdjoint
RAdjoint
Corr
Extensive
Reductive
Soundness
Optimality

Classical GCs
Posets
Mono. Functions
α:A →B
γ:B →A
id(x) ⊑ γ(y)
⇔ α(x) ⊑ id(y)
id ⊑ γ ◦ α
α ◦ γ ⊑ id
α ◦ f ◦ γ ⊑ f♯
α ◦ f ◦ γ = f♯

Kleisli/constructive GCs
Posets
℘-Monadic Functions
κα : A → ℘(B)
κγ : B → ℘(A)
ret(x) ⊆ κγ(y)
⇔ κα(x) ⊆ ret(y)
ret ⊑ κγ ⊛ κα
κα ⊛ κγ ⊑ ret
κα ⊛ f ⊛ κγ ⊑ f ♯
κα ⊛ f ⊛ κγ = f ♯

Computational

Constructive

Kleisli

Classical

Set inclusion
Theorem of choice

Figure 8. Relationship between classical, Kleisli and constructive
Lemma 1 (CGC-Induce).AGDAX For every Kleisli Galois connection hκα, κγi, there exists a constructive Galois connection hη, µi
where hpure(η), µi = hκα, κγi.

Figure 7. Comparison of constructive v classical adjunctions

Because the mapping from Kleisli to constructive is interesting we provide a proof, which to our knowledge is novel. The
proof builds a constructive Galois connection hη, µi from a Kleisli
hκα, κγi by exploiting the Kleisli correspondence and making use
of the constructive theorem of choice.

lifting operator on Kleisli Galois connections hκα, κγi∗ :
hα, γi = hκα, κγi∗ = hκα∗ , κγ ∗ i
This lifting is sound, meaning Kleisli soundness and optimality
results can be translated to classical ones.

Proof. To turn an arbitrary Kleisli Galois connection into a constructive one, we show that the effect on κα : A → ℘(B) is benign,
or in other words, that there exists some η such that κα = pure(η).
We prove this using two ingredients: a constructive interpretation of
the Kleisli extensive law, and the constructive theorem of choice.
We first expand the Kleisli expansive property, unfolding definitions of ⊛ and ret, to get an equivalent logical statement:

Theorem 1 (KGC-Sound). AGDAX For any Kleisli relationship of
soundness between f and f ♯ , that is κα ⊛ f ⊛ κγ ⊑ f ♯ , its
lifting to classical is also sound, that is α ◦ f ∗ ◦ γ ⊑ f ♯∗ where
hα, γi = hκα, κγi∗ , and likewise for optimality relationships.
This lifting is also complete, meaning classical Galois connection soundness and optimality results can always be translated to
Kleisli ones, when α and γ are of lifted form.

∀x.∃y.y ∈ κα(x) ∧ x ∈ κγ(y)

(KGC-Exp)

Statements of this form can be used in conjunction with an axiom
of choice in classical mathematics, which is:

Theorem 2 (KGC-Complete).AGDAX For any classical relationship
of soundness between f ∗ and f ♯∗ , that is α ◦ f ∗ ◦ γ ⊑ f ♯∗ , its
lowering to Kleisli is also sound when hα, γi = hκα, κγi∗ , that is
κα ⊛ f ⊛ κγ ⊑ f ♯ , and likewise for optimality relationships.

(∀x.∃y.R(x, y)) =⇒ (∃f.∀x.R(x, f (x)))

(AxChoice)

This theorem is admitted as an axiom in classical mathematics,
but in constructive logic—the setting used for extracting verified
algorithms–(AxChoice)is definable as a theorem, due to the computational interpretation of logical connectives ∀ and ∃. We define
(AxChoice) as a theorem in Agda without trouble:

Due to soundness and completeness, one can work with the simpler setup of Kleisli Galois connections without any loss of generality. The setup is simpler because Kleisli Galois connection theorems only quantify over individual elements rather than elements of
powersets. For example, the soundness criteria κα ⊛ f ⊛ κγ ⊑ f ♯
is proved by showing κα∗ (f ∗ (κγ(x))) ⊆ f ♯ (x) for an arbitrary
element x : A, whereas in the classical proof one must show
κα∗ (f ∗ (κγ ∗ (X))) ⊆ f ♯∗ (X) for arbitrary sets X : ℘(A).

choice : ∀{A B}{R : A → B → Set}
→ (∀ x → ∃ y st R x y)
→ (∃ f st ∀ x → R x (f x))
choice P = ∃ (λ x → π1 (P x)) , (λ x → π2 (P x))

Constructive Galois Connections Constructive Galois connections are a restriction of Kleisli Galois connections where the abstraction mapping is a pure rather than monadic function. We call
the left adjoint extraction, notated η, and the right adjoint interpretation, notated µ. The constructive Galois connection correspondence, alternative expansive and reductive formulation of the correspondence, and soundness and optimality criteria are identical to
Kleisli Galois connections where hκα, κγi = hpure(η), µi.

Applying (AxChoice) to (KGC-Exp) then gives:
∃η.∀x.η(x) ∈ κα(x) ∧ x ∈ κγ(η(x))

(ExpChioce)

which proves the existence of a pure function η : A → B.
In order to form a constructive Galois connection η and µ must
satisfy the correspondence, which we prove in split form:
x ∈ µ(η(x))
x ∈ µ(y) =⇒ η(x) ⊑ y

Constructive to Kleisli and Back Our main theorem which justifies the soundness and completeness of constructive Galois connections is an isomorphism between constructive and Kleisli Galois
connections. The easy direction is soundness, where a Kleisli Galois connection is formed by defining hκα, κγi = hpure(η), µi.
Soundness and optimality theorems are then lifted from constructive to Kleisli without modification.

(CGC-Exp)
(CGC-Red)

The expansive property is immediate from the second conjunct
in (ExpChioce). The reductive property follows from the Kleisli
reductive property:
x ∈ κγ(y) ∧ y ′ ∈ κα(x) =⇒ y ′ ⊑ y

(KGC-Red)

The constructive variant of reductive is proved by satisfying the first
two premises of (KGC-Red), where x ∈ κγ(y) is by assumption
and y ′ ∈ κα(x) is by the first conjunct in (ExpChioce).
So far we have shown that for a Kleisli Galois connection
hκα, κγi, there exists a constructive Galois connection hη, µi
where µ = κγ. However, we have yet to show pure(η) = κα.
To show this, we prove an analog of a standard result for classical
Galois connections: that α and γ uniquely determine each other.

Theorem 3 (CGC-Sound).AGDAX For any constructive relationship
of soundness between f and f ♯ , that is pure(η) ⊛ f ⊛ µ ⊑ f ♯ ,
its lifting to classical is sound, that is κα ⊛ f ⊛ κγ ⊑ f ♯ where
hκα, κγi = hpure(η), µi, and likewise for optimality relationships.
The other direction, completeness, is much more surprising.
First we establish a lowering for Kleisli Galois connections.

12

Lemma 2 (Unique Abstraction).AGDAX For any two Kleisli Galois
connections hκα1 , κγ1 i and hκα2 , κγ2 i, κα1 = κα2 iff κγ1 = κγ2

Deductive Synthesis Fiat [16] is a library for the Coq proof assistant which supports semi-automated synthesis of programs as refinements of their specifications. Fiat uses the same powerset type
and monad as we do, and their “deductive synthesis” process similarly derives correct-by-construction programs by calculus. Fiat
derivations start with a user-defined specification and calculate towards an under-approximation (⊒), whereas calculational abstract
interpretation starts with an optimal specification and calculates towards an over-approximation (⊑). It should be possible to generalize their framework to use partial orders to recover aspects of
our work, or to invert the lattice used in our abstract interpretation
framework to recover aspects of theirs. A notable difference in approach is that Fiat makes heavy use of Coq’s tactic programming
language to automate rewrites inside respectful contexts, whereas
our system provides no interactive proof automation and each calculational step must be justified explicitly.

We then conclude pure(η) = κα as a consequence of the above
lemma and the fact that µ = κγ.
Given the above mapping from Kleisli Galois connections to
constructive ones, we prove the completeness of this mapping.
Theorem 4 (CGC-Complete).AGDAX For any Kleisli relationship of
soundness between f and f ♯ , that is κα⊛f ⊛κγ ⊑ f ♯ , its lowering
to constructive is also sound, that is pure(η) ⊛ f ⊛ µ ⊑ f ♯ where
hη, µi is induced, and likewise for optimality relationships.
Mechanization We mechanize the metatheory for constructive
Galois connections and both case studies from Sections 4 and 5
in Agda, as well as a general purpose proof library for posets and
calculational reasoning with the monotonic powerset monad. The
development is available at: github.com/plum-umd/cgc.

Monadic Abstract Interpretation Monads in abstract interpretation have recently been applied to good effect for modularity [15,
31]. However, that work uses monads to structure the semantics,
not the Galois connections and proofs.

Wrapping Up In this section we showed that constructive Galois
connections are sound w.r.t. classical Galois connections, and complete w.r.t. the subset of classical Galois connections recovered by
lifting constructive ones. We showed this by introducing an intermediate space of Galois connections, Kleisli Galois connections,
and by establishing two sets of isomorphisms between a subset
of classical and Kleisli, and between Kleisli and constructive. The
proof of isomorphism between constructive and Kleisli yielded an
interesting proof which applies the constructive theorem of choice
to one of the Kleisli Galois connection correspondence laws.

Future Directions Now that we have established a foundation
for constructive Galois connection calculation, we see value in
verifying larger derivations (e.g. [23, 30]). Furthermore we would
like to explore whether or not our techniques have any benefit in
the space of general-purpose program calculations à la Bird.
Currently our framework requires the user to justify every detail of the program calculation, including monotonicity proofs and
proof scoping for rewrites inside monotonic contexts. We imagine
much of this can be automated, requiring the user to only provide
the interesting parts of the proof, à la Fiat[16]. Our experience has
been that even Coq’s tactic system slows down considerably when
automating all of these details, and we foresee using proof by reflection in either Coq (e.g. Rtac [20]) or Agda to automate these
proofs in a way that maintains proof-checker performance.
There have been recent developments on compositional abstract
interpretation frameworks [15] where abstract interpreters and their
proofs of soundness are systematically derived side-by-side. That
framework relies on correctness properties transported by Galois
transformers, which we posit would benefit from mechanization
since they hold both computational and specification content.

7. Related Work
This work connects two long strands of research: abstract interpretation via Galois connections and mechanized verification via
dependently typed functional programming. The former is founded
on the pioneering work of Cousot and Cousot [11, 12]; the latter on
that of Martin-Löf [21], embodied in Norell’s Agda [28]. Our key
technical insight is to use a monadic structure for Galois connections, following the example of Moggi [25] for the λ-calculus.
Calculational Abstract Interpretation Cousot describes calculational abstract interpretation by example in his lecture notes [9] and
monograph [8], and recently introduced a unifying calculus for Galois connections [14]. Our work mechanizes Cousot’s calculations
and provides a foundation for mechanizing other instances of calculational abstract interpretation (e.g. [22, 30]). We expect our work
to have applications to the mechanization of calculational program
design [2, 3] by employing only Galois retractions, i.e. α ◦ γ is an
identity [14]. There is prior work on mechanized program calculation [33], but it is not based on abstract interpretation.

8. Conclusions
This paper realizes the vision of mechanized and constructive Galois connections foreshadowed by Cousot [8, p. 85], giving the first
mechanically verified proof by calculational abstract interpretation;
once for his generic static analyzer and once for the semantics of
gradual typing. Our proofs by calculus closely follow the originals.
The primary discrepancy is the use of monads to isolate specification effects. By maintaining this discipline, we are able to verify calculations by Galois connections and extract computational content
from pure results. The resulting artifacts are correct-by-verifiedconstruction, thereby avoiding known bugs in the original.2

Verified Static Analyzers Verified abstract interpretation has
many promising results [1, 5, 6, 29], scaling up to large-scale realworld static analyzers [18]. However, mechanized abstract interpretation has yet to benefit from the Galois connection framework.
Until now, approaches use classical axioms or “γ-only” encodings of soundness and (sometimes) completeness. Our techniques
for mechanizing Galois connections should complement these approaches.

Acknowledgments
We thank Ron Garcia and Éric Tanter for discussions of their work.
Éric also helped with our French translation. We thank the Colony
Club in D.C. and the Board & Brew in College Park for providing
fruitful environments in which to work. We thank the anonymous
reviewers of ICFP 2016 for their helpful feedback. This material is
partially based on research sponsored by DARPA under agreement
number AFRL FA8750-15-2-0104.

Galculator The Galculator [32] is a proof assistant founded on
an algebra of Galois connections. This tool is similar to ours in
that it mechanically verifies Galois connection calculations. Our
approach is more general, supporting arbitrary set-theoretic reasoning and embedded within a general purpose proof assistant, however their approach is fully automated for the small set of derivations which reside within their supported theory.

2 di.ens.fr/~cousot/aisoftware/Marktoberdorf98/Bug History

13

References

the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages, POPL 2015. ACM, 2015.

[1] G. Barthe, D. Pichardie, and T. Rezk. A certified lightweight noninterference java bytecode verifier. In R. D. Nicola, editor, Programming Languages and Systems, Lecture Notes in Computer Science.
Springer Berlin Heidelberg, 2007.
[2] R. Bird and O. de Moor. The Algebra of Programming. Prentice Hall,
1996.
[3] R. S. Bird. A calculus of functions for program derivation. In D. A.
Turner, editor, Research Topics in Functional Programming. AddisonWesley, 1990. Also available as Technical Monograph PRG-64, from
the Programming Research Group, Oxford University.
[4] B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné,
D. Monniaux, and X. Rival. A static analyzer for large safety-critical
software. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’03. ACM,
2003.

[17] R. Garcia, A. M. Clark, and É. Tanter. Abstracting gradual typing.
In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages (POPL 2016), St Petersburg,
FL, USA, Jan. 2016. ACM Press. To appear.
[18] J. H. Jourdan, V. Laporte, S. Blazy, X. Leroy, and D. Pichardie. A
Formally-Verified c static analyzer. In Proceedings of the 42Nd Annual
ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL ’15. ACM, 2015.
[19] X. Leroy. Formal verification of a realistic compiler. Commun. ACM,
2009.
[20] G. Malecha and J. Bengtson. Extensible and efficient automation
through reflective tactics. In Programming Languages and Systems
- 25th European Symposium on Programming, ESOP 2016. Springer,
2016.
[21] P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.
[22] J. Midtgaard and T. Jensen. A calculational approach to Control-Flow
analysis by abstract interpretation. In M. Alpuente and G. Vidal, editors, Static Analysis, Lecture Notes in Computer Science, chapter 23.
Springer Berlin Heidelberg, 2008.

[5] S. Blazy, V. Laporte, A. Maroneze, and D. Pichardie. Formal verification of a c value analysis based on abstract interpretation. In F. Logozzo and M. Fähndrich, editors, Static Analysis, Lecture Notes in
Computer Science. Springer Berlin Heidelberg, 2013.
[6] D. Cachera and D. Pichardie. A certified denotational abstract interpreter. In M. Kaufmann and L. Paulson, editors, Interactive Theorem
Proving, Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2010.
[7] P.
Cousot.
Abstract
interpretation.
URL
http://www.di.ens.fr/~ cousot/AI/.

[23] J. Midtgaard and T. Jensen. A calculational approach to ControlFlow analysis by abstract interpretation. In M. Alpuente and G. Vidal,
editors, Static Analysis Symposium, LNCS. Springer, 2008.
[24] A. Miné. The octagon abstract domain. Higher-Order and Symbolic
Computation, 2006.
[25] E. Moggi. An abstract view of programming languages. Technical
report, Edinburgh University, 1989.

[8] P. Cousot. The calculational design of a generic abstract interpreter. In
M. Broy and R. Steinbrüggen, editors, Calculational System Design.
NATO ASI Series F. IOS Press, Amsterdam, 1999.

[26] D. Monniaux. Réalisation mécanisée d’interpréteurs abstraits. Rapport de DEA, Université Paris VII, 1998. French.
[27] F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program
Analysis. Springer-Verlag, 1999.

[9] P. Cousot. MIT 16.399: Abstract interpretation, 2005.
[10] P. Cousot and R. Cousot. Static determination of dynamic properties
of programs. In 2nd International Symposium on Programming, 1976.
[11] P. Cousot and R. Cousot. Abstract interpretation: a unified lattice
model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN
Symposium on Principles of Programming Languages. ACM, 1977.

[28] U. Norell. Towards a practical programming language based on
dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412
96 Göteborg, Sweden, Sept. 2007.
[29] D. Pichardie. Interprétation abstraite en logique intuitionniste: extraction d’analyseurs Java certifiés. PhD thesis, Université Rennes,
2005.
[30] I. Sergey, J. Midtgaard, and D. Clarke. Calculating graph algorithms
for dominance and shortest path. In J. Gibbons and P. Nogueira, editors, Mathematics of Program Construction, Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2012.
[31] I. Sergey, D. Devriese, M. Might, J. Midtgaard, D. Darais, D. Clarke,
and F. Piessens. Monadic abstract interpreters. In Proceedings of the
34th ACM SIGPLAN Conference on Programming Language Design
and Implementation. ACM, 2013.

[12] P. Cousot and R. Cousot. Systematic design of program analysis
frameworks. In Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’79. ACM,
1979.
[13] P. Cousot and R. Cousot. Inductive definitions, semantics and abstract
interpretations. In Proceedings of the 19th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL ’92.
ACM, 1992.
[14] P. Cousot and R. Cousot. A Galois connection calculus for abstract
interpretation. In Proceedings of the 41st ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL ’14.
ACM, 2014.

[32] P. F. Silva and J. N. Oliveira. ‘Galculator’: Functional prototype of a
Galois-connection based proof assistant. In Proceedings of the 10th
International ACM SIGPLAN Conference on Principles and Practice
of Declarative Programming, PPDP ’08. ACM, 2008.

[15] D. Darais, M. Might, and D. Van Horn. Galois transformers and modular abstract interpreters. In Proceedings of the 2015 ACM SIGPLAN
International Conference on Object-Oriented Programming, Systems,
Languages, and Applications, OOPSLA 2015, pages 552–571. ACM,
2015.
[16] B. Delaware, C. Pit-Claudel, J. Gross, and A. Chlipala. Fiat: Deductive
synthesis of abstract data types in a proof assistant. In Proceedings of

[33] J. Tesson, H. Hashimoto, Z. Hu, F. Loulergue, and M. Takeichi. Program calculation in Coq. In M. Johnson and D. Pavlovic, editors,
Algebraic Methodology and Software Technology, Lecture Notes in
Computer Science, chapter 10. Springer Berlin Heidelberg, 2011.

14

