# Abstract Interpreters: A Monadic Approach to Modular Verification

Sébastien Michelland, Yannick Zakowski, Laure Gonnord

► To cite this version:

Sébastien Michelland, Yannick Zakowski, Laure Gonnord. Abstract Interpreters: A Monadic Approach to Modular Verification. Proceedings of the ACM on Programming Languages, 2024, 8 (ICFP), pp.1-28. 10.1145/3674646. hal-04628727

HAL Id: hal-04628727

https://hal.science/hal-04628727v1

Submitted on 28 Jun 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Abstract Interpreters: A Monadic Approach to Modular
Verification

SÉBASTIEN MICHELLAND, Université Grenoble-Alpes, Grenoble INP, LCIS, France

YANNICK ZAKOWSKI, Inria, France

LAURE GONNORD, Université Grenoble-Alpes, Grenoble INP, LCIS, France

We argue that monadic interpreters built as layers of handlers stacked atop the free monad, as advocated notably by the ITree library, also constitute a promising way to implement and verify abstract interpreters in dependently-typed theories such as the one underlying the Coq proof assistant.

The approach enables both code reuse across projects and modular proofs of soundness of the resulting interpreters. We provide generic abstract control flow combinators proven correct once and for all against their concrete counterpart. We demonstrate how to relate concrete handlers implementing effects to abstract variants of these handlers, essentially capturing the traditional soundness of transfer functions in the context of monadic interpreters. Finally, we provide generic results to lift soundness statements via the interpretation of stateful and failure effects.

We formalize all the aforementioned combinators and theories into a Coq library, and demonstrate their benefits by implementing and proving correct two illustrative abstract interpreters respectively for a structured imperative language and a toy assembly.

CCS Concepts: • **Theory of computation** → **Logic and verification**; **Denotational semantics**; • **Software and its engineering** → **Formal software verification**.

Additional Key Words and Phrases: Monadic Semantics, Abstract Interpretation, Formal Verification

**ACM Reference Format:**

Sébastien Michelland, Yannick Zakowski, and Laure Gonnord. 2024. Abstract Interpreters: A Monadic Approach to Modular Verification. *Proc. ACM Program. Lang.* 8, ICFP, Article 257 (August 2024), 28 pages. https://doi.org/10.1145/3674646

# 1 INTRODUCTION

The realm of mechanized verification of programming languages has reached a staggering degree of maturity. Backing up meta-theoretical results with a formalization in a proof assistant has become increasingly routine in the programming language research community [Ringer et al. 2019]. But such formalization efforts have not only become more common, they have grown in scale and ambition: large-scale software is verified against faithful semantics of existing industrial-strength languages [Gu et al. 2016; Jung et al. 2017; Kumar et al. 2014; Leroy 2009].

When it comes to formalized proofs, details of representation matter greatly. Propositionally specified transition systems are by and large the most popular: typically, the small-step semantics is specified through proof rules, using a binary relation between dynamic configurations, and its transitive closure describes executions. While extremely successful, such approaches have drawbacks. On the practical side, these semantics are non-executable at their core, hence requiring significant extra work to support crucial practice such as differential testing against industrial reference interpreters. In reaction, frameworks such as Skeletal Semantics [Bodin et al. 2019] or

Authors' Contact Information: Sébastien Michelland, sebastien.michelland@lcis.grenoble-inp.fr, Université Grenoble-Alpes, Grenoble INP, LCIS, France; Yannick Zakowski, yannick.zakowski@inria.fr, Inria, France; Laure Gonnord, laure.gonnord@grenoble-inp.fr, Université Grenoble-Alpes, Grenoble INP, LCIS, France.

© 2024 Copyright held by the owner/author(s).

This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in *Proceedings of the ACM on Programming Languages*, https://doi.org/10.1145/3674646.
the K framework [Rosu and Serbanuta 2010] have been designed notably in order to support the automatic derivation of executable interpreters from the formal semantics. On the theoretical side, they tend to lack support for equational reasoning, and often give up on compositionality-recursive definition on the syntax-and modularity-independent definition and combination of the features of the language.

These shortcomings become increasingly painful when formal developments scale. In contrast, when applicable, monads and subsequently algebraic effects have long been recognized as an appealing approach to modeling the semantics of effectful programs. The monad laws, extended with algebraic domain-specific equations capturing the semantics of the effects at hand, yield powerful reasoning principles. Monads have been both a pen-and-paper theoretical tool and a practical programming paradigm for decades, but have also become increasingly popular in the mechanized realm. In particular, *free monads* [Swierstra 2008] have been at the root of flexible, general-purpose reasoning frameworks. Variations on this idea have appeared throughout the literature, for instance as the *program monad* in the FreeSpec project [Letan et al. 2018], as *I/O-trees* [Hancock and Setzer 2000], and as *McBride's general monad* [McBride 2015].

In this paper, we focus on *interaction trees* [Xia et al. 2020] (ITrees), a recent realization of this approach as a Coq library. ITrees are defined as a coinductive variant of the *freer monad* [Kiselyov and Ishii 2015] and are also closely related to *resumption monads* [Piróg and Gibbons 2014]. The library provide rich reusable components to model and reason about effectful, recursive, interactive computations, while supporting extraction. In particular, they make the definition of denotational semantics for first-order languages with first-order effects straightforward.

ITrees have been applied in a wide range of projects, such as modeling network servers [Koh et al. 2019; Zhang et al. 2021], transactional objects [Lesani et al. 2022], concurrency [Chappe et al. 2023], or non-interference [Silver et al. 2023]. Their largest application is arguably the Vellvm project [Zakowski et al. 2021; Zhao et al. 2012], providing a compositional, modular and executable semantics for a large sequential subset of LLVM's intermediate representation. This application leverages the approach's modularity heavily, structuring the semantics into a series of layers, each plugging in an independent implementation of a feature of the language.

In the present work, we seek to offer similar benefits of modularity and reusable components for writing static analyses against ITree-based formal semantics and proving their soundness. We place ourselves more specifically in the *abstract interpretation* framework [P. Cousot 2021; P. Cousot and R. Cousot 1979]. Abstract interpretation is well known for providing rich ways of combining abstractions, through products [Cortesi et al. 2013] or communication-based protocols [P. Cousot, R. Cousot, et al. 2006; Jourdan et al. 2015]. In this paper, we do not focus our attention on such construction of rich abstract domains. Rather, we follow the *big-step abstract interpreter* line of works [Bodin et al. 2019; D. Darais, Labich, et al. 2017; Keidel and Erdweg 2019; Keidel, Poulsen, et al. 2018] in seeking to provide rich reusable combiners to lighten the construction of *verified abstract interpreters*.

Our contributions can be crystallized as follows:

* we demonstrate that the paradigm of defining languages as layered monadic interpreters can be used to simultaneously define a concrete and an abstract interpreter from a single denotation of the source language;

* we identify that parameterizing abstract interpretation algorithms over the concrete language's monadic effects is key to this construction, and formalize a monad of abstract control flow *aflow* capturing this idea;
* we express a notion of soundness applicable to layered monadic interpreters at intermediate stages of their definition, which enables certification from composing independent soundness proofs for each language feature;

* we provide a Coq implementation of the scheme as a reusable library, featuring a number of pre-certified abstract interpretation algorithms;

* finally, we showcase this work by modularly certifying abstract interpreters for a standard IMP language and (in the linked artifact) a toy assembly language.

Our Coq development with meta-theoretical results and the library is available as open-source software.

Section 2 starts by providing necessary background on ITrees and abstract interpretation. Section 3 presents an overview of the library through the motivating example of a small IMP language. Section 4 illustrates the challenges and motivates our design, whose programmatic component is described in more detail in Section 5. Finally, Section 6 provides details on the meta-theory, and the process of certifying an abstract interpreter from the perspective of a user of our library. We conclude with related work and a quick summary.

# 2 BACKGROUND

Typographic remarks. For clarity and conciseness, we take some light liberties with Coq code included in this paper. When clear from context, we omit implicit arguments. We use mathematical notations in lieu of traditional identifiers. Furthermore, we present simplified versions of the code such as specialized definitions where the artifact is parametrized, or Fixpoint instead of Equations. To clear any accidental confusion, we systematically reference the accompanying code with hyperlinks symbolized by ().<fnref n="1" /> We make use of functions between type families, writing $E \stackrel{\sim}{\to} F ::= \forall \{X\}, E X \to F X$ for such a function between $E, F: Type \to Type$. We write $\mathbf{1}$ and $(\cdot)$ for the unit type and its inhabitant.

## 2.1 Interaction Trees and Monadic Interpreters

Interaction Trees [Xia et al. 2020] (ITrees) have emerged in the Coq ecosystem as a rich toolbox for building compositional and modular monadic interpreters for first order languages. The library also provides an equational theory for reasoning about equivalence and refinement of computations. Through this section, we introduce the programmatic side of this framework.

ITrees are a data structure for representing computations interacting with an external environment through visible events, defined as:

```
CoInductive itree (E: Type → Type) (R: Type) : Type ::=
  | Ret (r: R)                      (* terminating computation *)
  | Tau (t: itree E R)              (* "silent" tau transition *)
  | Vis {A: Type} (e : E A) (k : A → itree E R). (* event e yielding an answer in A *)
```

The datatype takes two parameters: a signature $E$ that specifies the set of interactions the computation may have with the environment, and the type $R$ of values that it may return. ITree computations can be thought of as trees built out of three constructors. Leaves, via the Ret constructor, model pure computations, return values of type $R$. Vis nodes model an effect being performed, before yielding to the continuation $k$ with the value resulting from $e$. Finally, ITrees are defined coinductively, allowing them to model diverging computations as non-well-founded trees. Accordingly, the Tau constructor represents a non-observable internal step that occurs, much as in Capretta's delay monad [Capretta 2005].

<footnote n="1">¹https://gitlab.inria.fr/sebmiche/itree-ai</footnote>
(*) Embedding of pure computations *)
ITree.ret (r: R): itree E R := Ret r.
(*) Sequencing computations *)
ITree.bind (u: itree E T) (k: T → itree E U): itree E U.
(*) Atomic execution of an event. *)
ITree trigger: E ↛ itree E := fun e ⇒ Vis e Ret.
(*) Fixed-point combinator *)
ITree.iter (body: I → itree E (I+R)): I → itree E R.

<caption>Fig. 1. ITrees: type signature of the main combinators</caption>

op ∈ Op ::= ⊕ | ∨ | ⊗
e ∈ E ::= x ∈ X | v ∈ V | e₁ op e₂
s ∈ C ::= skip | assert e | x := e | s₁; s₂ | if e then s₁ else s₂ | while e do s

<caption>Fig. 2. IMP: abstract syntax (笑)</caption>

One may think of ITrees as a low level imperative programming language embedded inside
Gallina. The library exposes the primitive combinators shown in Figure 1. ITrees have a monadic
structure: pure computations can be embedded via `ret`, and computations can be sequenced with
the traditional `bind` construct.<fnref n="2" /> A minimal effectful computation can be written `ITree.trigger e`
yielding control to the environment to perform an effect `e` and returning the result. By virtue
of their coinductive nature, ITrees form what is sometimes referred to as a completely iterative
monad [Aczel et al. 2003]. From the eye of the programmer, this captures the ability to write fixpoints
using the `iter` combinator. Operationally, `iter f i` is the computation repeatedly performing `f i`
each time checking whether the result is a new accumulator `inl j` and continuing with `iter f j`,
or if it is a final value `inr r` and returning `r`.

To make things concrete, we turn to our main running example: a traditional IMP language [Pierce
et al. 2018] whose abstract syntax is depicted on Figure 2. Arithmetic expressions contain variables
in X, literals in V and binary operations. Statements include the usual assignments, sequencing,
conditionals and loops, as well as an assert statement acting as a no-op if the condition is nonzero
and failure otherwise.

We model IMP's dynamic semantics using ITrees in Figure 3. The process, already illustrated
in [Xia et al. 2020], and at scale notably in Vellvm [Zakowski et al. 2021], is split into two main
phases.

*Denotation.* We first want to denote the syntax into an interaction tree. At this stage, events are still symbolic (one can think of them as the labels in a labeled transition system modeling the program). The “Event signature” section of Figure 3 shows the three features for which we choose to use events in IMP:<fnref n="3" />

* Arithmetic (arithE) for binary arithmetic computations. The Compute event takes the parameters to the operation and returns a value.

* Memory access (memE) for reading and writing variables. Read x returns a value while Write x v returns unit. Both will access the global memory state as a side-effect once implemented.

* Assertions (assertE). Assert v evaluates that v is non-zero and returns unit. It causes the program to fail and abort as a side-effect if v is zero.

We call E the disjoint sum of these events, which forms the full event signature of IMP.

<footnote n="2">²We use `x ← c;;` `k x` as a notation for `bind c (fun x ⇒ k x)`.</footnote>

<footnote n="3">³ITrees also hardcode divergence in the structure, making it available at all times.</footnote>
<figure><img src="image_2.png" /><figcaption>Fig. 3. IMP: Building an ITree-based concrete interpreter</figcaption></figure>

We can then move on to the denotation functions, defined by recursion on the syntax tree. The code is mostly straightforward for expressions, with only binary computations requiring multiple steps, and closely resembles a monadic interpreter as one would write e.g. in Haskell. Statements are more of the same, but notice the use of *control-flow combinators* `cond` and `while` to implement conditionals and loops. The ternary `cond` combinator simply desugars to a Coq-level `if` construct. The only subtlety resides in the representation of loops: we define on top of `iter` a `while` combinator using the accumulator as a single bit of information informing the combinator when to escape:
Definition while (guard: itree E V) (body: itree E 1) :=
ITree.iter (fun (_: 1) ) ⇒
v ← guard;;
if v =? 0 then ITree.ret (inr())
else body;; ITree.ret (inl())

We emphasize this notion of control flow combiners because they will later be key to the definition and proof of abstract interpreters.

Handling. By representing IMP’s abstract syntax as ITrees, we have given a semantics to its control flow, but its effects remain purely syntactic. We now provide handlers for each category of effects, implementing them through an appropriate monad transformer.

The arithmetic operations we consider here are pure, hence h_arith does not introduce any transformer; it only relies on a pure implementation compute_binop omitted here. Memory interactions are stateful, which we implement with the traditional state transformer over a concrete state s : S providing mem_store and mem_get operations (the latter returning 0 for undefined values). Finally, asserts may fail, hence henk introduces failure via the usual failT transformer. These additions of monadic transformers enable the implementation of events’ side-effects as pure computations.

We are finally ready to define our concrete interpreter for IMP, eval, by successively handling all three layers of effects. Each handling removes an event family from the signature and adds a monad transformer. The resulting semantic domain is hence failT (stateT S (itree 0)) (where 0 is the empty signature), i.e. a stateful computation that may fail (or diverge).

Getting there requires two final ingredients. First, the hoist monadic combinator lifts a monad morphism f: m ⇝ n under a transformer t, giving us hoist f: t m ⇝ t n. This allows us to chain our monad transformations. Second, ITrees’ handle function<fnref n="4" /> applies an event handler to a program:

handle (h: E ↦ M): itree E ↦ M.

In this paper, M will always be monadT (itree F) for some monad transformer monadT and a smaller
event signature F. For clarity, we write handle_state, handle_fail, etc. to recall the monad trans-
former being applied with each use of the function. handle substitutes events with the specified
handler’s implementation and applies the monadic transformer transparently. Putting all the ingre-
dients together, we get the eval function from the end of Figure 3, which is a concrete interpreter
for IMP.

When evaluated on an IMP program and an initial state, eval returns an option (S * 1), i.e. the
final state and return value, if the program doesn’t fail. We can obtain an executable interpreter by
using Coq’s extraction feature.

This way of defining an interpreter allows one to decouple the various features of the language,
which scales better for building and reasoning about complex languages, as exemplified by Vel-
lvm [Zhao et al. 2012]. Hence, we are interested in doing the same for static analyzers, specifically
abstract interpreters.

## 2.2 Abstract Interpretation

Abstract interpretation [P. Cousot and R. Cousot 1979] provides a simple and elegant way to compute sound approximations of a program’s semantics, by mimicking the concrete evaluation of the program in an abstract fashion. The analysis defines an over-approximation of the set of states and control flow of the concrete program, trading accuracy in exchange for guaranteed termination.

<footnote n="4">⁴The function is called interp in the ITree library. We reserve the words interpreter and interpretation for the resulting concrete or abstract executable process through this paper to avoid any confusion.</footnote>
<table><caption>Fig. 4. Common lattice operations and numerical domain for IMP. V and V# represent concrete and abstract values. The measure order is lexicographic for both measure axioms.</caption><thead><tr><th>Operation or relation</th><th>Axioms (implicitly quantified on c, x, y)</th></tr></thead><tbody><tr><td>∈: V → V<sup>#</sup> → Prop</td><td>Relates to the Galois connection by ∀v, v ∈ x ≜ v ∈ γ(x)</td></tr><tr><td>⊆?: V<sup>#</sup> → V<sup>#</sup> → bool</td><td>Preorder c ∈ x → x ⊑? y → c ∈ y</td></tr><tr><td>join (∪): V<sup>#</sup> → V<sup>#</sup> → V<sup>#</sup></td><td>x ⊑ x ∪ y y ⊑ x ∪ y</td></tr><tr><td>meet (∪): V<sup>#</sup> → V<sup>#</sup> → V<sup>#</sup></td><td>v ∈ x → v ∈ y → v ∈ x ∩ y</td></tr><tr><td>widen: V<sup>#</sup> → V<sup>#</sup> → V<sup>#</sup></td><td>x ⊑ widen x y y ⊑ widen x y</td></tr><tr><td>measure_N: nat</td><td>measure (widen x y) ≤ measure x</td></tr><tr><td>measure: V<sup>#</sup> → nat<sup>measure_N</sup></td><td>¬(y ⊑? x) → measure (widen x y) < measure x</td></tr><tr><td>⊤, ⊥: V<sup>#</sup></td><td>∀v, v ∈ ⊤ measure ⊤ = (0, ..., 0)</td></tr><tr><td>const: V → V<sup>#</sup></td><td>v ∈ const v</td></tr><tr><td>istrue, isfalse: V<sup>#</sup> → bool</td><td>istrue x → v ∈ x → v ≠ 0 isfalse x → v ∈ x → v = 0</td></tr><tr><td>opp: V<sup>#</sup> → V<sup>#</sup></td><td>v ∈ x → -v ∈ opp x</td></tr><tr><td>add, sub: V<sup>#</sup> → V<sup>#</sup> → V<sup>#</sup></td><td>v<sub>1</sub> ∈ x<sub>1</sub> → v<sub>2</sub> ∈ x<sub>2</sub> → v<sub>1</sub> {+, -} v<sub>2</sub> ∈ {add, sub} x<sub>1</sub> x<sub>2</sub></td></tr></tbody></table>

An abstract domain defines approximations of program objects (values); for simplicity in this paper we consider non-relational numerical domains. To further exemplify, we shall consider the Interval domain, which abstracts sets of numerical values $V \subseteq \mathbb{Z}^d$ by $V^# \subseteq \text{Interval}^d$, where $\text{Interval} = (\mathbb{Z} \cup \{-\infty\}) \times (\mathbb{Z} \cup \{+\infty\})$.

We use the standard formalization of domains as lattices equipped with union (join, ∪), minimal and maximal elements (⊥, ⊤), and a decidable order denoted by ⊑?. A pair of abstraction and concretization functions ($\alpha: \mathcal{P}(V) \to V^#$, $\gamma: V^# \to \mathcal{P}(V)$) forming a Galois connection is expected to relate the abstract domain to the concrete one, although we follow Pichardie's γ-only encoding [Pichardie 2005] as summed up in Figure 4. The first half of the table lists the interface for lattice types in our implementation, with required axioms on the second column. The second half lists the interface for abstractions of numerical types such as integers.

To ensure termination during the analysis of loops, abstract domains come with a widening operator equipped with a well-founded measure over vectors of naturals. It implies the common widening insurance of “non-infinite increasing sequence of abstract values” [Rival and Yi 2020].

Abstract interpretation has mainly two implementation variants; we elect to expose here in pseudo-code “big-steps abstract interpretation”, which “mimics” the big steps operational semantics of a language and replaces each concrete operation with its abstract counterpart. As for IMP, abstract interpretation with the Interval abstract domain computes and propagate an Interval for each variable (in $\mathcal{X}$) of the program.

Assignment $x := e$ simply performs an explicit update for $x$ in the memory $m^#$:

$$ [[x := e]^#(m^#) = v^# \leftarrow [[e]^# \qquad \text{return } m^#[x := v^#].] $$

Abstract skip is a no-op, abstract sequence is also a sequence in the interpreter. Conditionals must run both branches independently (from the same initial memory) and join the results (here not showing the case of decidable conditions):<fnref n="5" />

$$ [[\text{if e then } s_1 \text{ else } s_2]^#(m^#) = \begin{aligned}[t] & m_1^# \leftarrow [[s_1]^#(m^#) \\ & m_2^# \leftarrow [[s_2]^#(m^#) \\ & \quad \text{return } (m_1^# \sqcup m_2^#) \end{aligned} $$

<footnote n="5">⁵We ignore guards in conditions and loops for now because the expression language will be user-supplied and inverting arbitrary expressions is beyond the scope of this contribution.</footnote>
Loops `while e do s` could naively perform an unbounded number of (abstract) iterations. Termination is hence ensured by the usage of the widening operator, which converges due to its well-founded measure:

$$ 
\begin{align*}
[\text{while } e \text{ do } s]^{\#}(m^{\#}) &= \text{repeat } m_{1}^{\#} \leftarrow [\text{s}]^{\#}(m^{\#}) \\
& \quad m_{2}^{\#} \leftarrow \text{widen } m^{\#} (m^{\#} \sqcup m_{1}^{\#}) \\
& \quad \text{if } (m_{2}^{\#} \subseteq m^{\#}) \\
& \qquad \text{return } m^{\#} \\
& \quad m^{\#} \leftarrow m_{2}^{\#}.
\end{align*}
$$

That is, `[while e do s]^{#}(m^{#})` is the least fixpoint of iterating the loop body with widening, applied on $m^{#}$.

From these ingredients (replacing computations with abstract domain operations and control flow with specific algorithms), the abstract interpretation framework [P. Cousot and R. Cousot 1979] guarantees that the computation of the abstract semantics *always terminates* and is *safe*, in the sense that the concretization of the obtained semantics is always larger than the (usually intractable) concrete semantics.

We aim to fit this framework into a layered, monadic setting, in the style of Section 2.1. Looking back, we can superficially notice that we would like to be able to see assignment as an effect, but also that the control flow of the abstract interpreter differs vastly from the concrete one: in particular, the required independent execution of branches seems at first incompatible with the naive threading of state through binds. The ITrees toolkit seems to fall short: we illustrate how to nonetheless recover similar techniques.

## 3 A TASTE OF OUR LIBRARY

Before getting into technical challenges and our solutions, let us illustrate the end result of using our library to simultaneously define a concrete and abstract interpreters for `IMP` (A). The code for this, given in Figure 5, is similar to Section 2.1 but derives both interpreters from a single representation.

Having previously defined concrete events and their handlers, we now define matching abstract events and their handlers. Some of these definitions are shared; for instance, the memory and arithmetic handlers are parameterized on a map data structure and a numerical type respectively, and their abstract implementation is identical to their concrete one. For `hlds` however, the implementation differs because the abstract failure monad transformer `failT` is different from the standard `failT`: instead of adding failure to the analyzer, it turns return values into pairs of an error value and a normal value. The *error value* indicates whether the failure path might have been taken, while the *normal value* approximates the concrete program's return value in non-failing cases—we come back to `failT`'s definition in Section 5.1. The `hlds` handler attempts to decide the assertion's condition using functions from the `NumericalDomain` class (which is implemented by `V` but not shown here) before returning such a pair.

We then proceed to denote `IMP` again, except this time we produce an object of the library-provided type `SurfaceAST E E# 1 1# b`,<fnref n="6" /> whose definition we delay until Section 5.2. Elements of this datatype can be thought of as mixed representations that can be projected into either a concrete or an abstract denotation depending on the value of `b`. This duality is most apparent in the `ret-and` and `do-and` (event) statements, where both the concrete and the abstract values or events are provided.

As with the denotation from Section 2.1, control flow in this representation relies on predefined combinators, here `AST_if` and `ASTwhile_unit`. The name `SurfaceAST` comes from the fact that these

<footnote n="6">⁶`1#` is the two-element unit lattice.</footnote>
Naturally, there is another side to this coin; we can now as easily extract an abstract program, which is represented into another monad, dubbed *aflow* (a):

ast2aflow: SurfaceAST E E# R R# true → aflow E R.

This new structure, a monad for abstract-interpretation control flow, will be thoroughly motivated through Section 4 and formally defined in Section 5.1. We shall show (also in Section 5.1) that it supports its own notion of event handling, allowing us to mirror the handling process of the concrete interpreter. An executable abstract interpreter in the form of an ITree is obtained by eventually unfolding control flow structures after handling abstract events (unfold, defined in Section 5.1).

*Proving sound the abstract interpreter.* All in all, we provide tools to define concrete and abstract interpreters simultaneously in Coq as layered monadic interpreters. This is not all, however—we also prove the abstract interpreter’s soundness! For pairs of denotations derived from a shared SurfaceAST, the library proves the soundness of control flow structures and allows users to derive the soundness of the abstract interpreter with minimal obligations. These are, specifically: values returned in *ret-and* and events emitted in *do-and* should be related by the appropriate Galois connection; and (more importantly) abstract event handlers should be sound w.r.t. their concrete counterparts. Section 6 is dedicated to making this claim precise and substantiated.

*Running the abstract interpreter.* Since ITrees are executable, we can extract the proven sound abstract interpreter into an OCaml program using Coq’s extraction feature<fnref n="7" /> and run it as a standalone program (a). As a minimal example, consider the following IMP program:

```
x := 2; y := 0;
while x do { y := 1; x := sub(x, 1); }
z := 5; assert(y); z := 6;
```

The analyzer returns a final state indicating $x \in (-\infty, 2], y \in \{0, 1\}$ and $z \in \{5, 6\}$. The lack of a lower bound on $x$ is the direct result of widening after decrementing in the loop. The simple abstract condition we use does not notice the decidable condition in the first iteration, thus allowing $y = 0$. This causes the assert to be analyzed as potentially failing, so the final state (which might be at the assert) has either $z = 5$ or $z = 6$.

*Another case study: Asm (a).* To illustrate the expressivity of our framework, we also write and prove correct an abstract interpreter for Asm, a toy control flow graph language featuring registers and memory. This language presents two layers of handling into the state monad and is centered around a CFG control flow structure (also provided by the library). Both its definition and proof are very similar to that of IMP’s, and in fact the theorems for the soundness of memory handling are shared.

# 4 DESIGN OF A LAYERED ABSTRACT INTERPRETER

We now discuss the theoretical ideas that enable the construction of a layered abstract interpreter in Figure 5 and its modular proof of soundness. This section focuses on how the integration of monadic event handling influences the design of the abstract interpreter. We build up to Figure 6, which provides a bird’s-eye view of the dual concrete/abstract denotation process, and Figure 7, which explains control flow structures that are key to our support for event handling. These figures will underpin our presentation of the Coq implementation and proof in Sections 5 and 6.

<footnote n="7">⁷Naturally, we can also extract the concrete interpreter, as is usual.</footnote>
<figure><img src="image_3.png" /><figcaption>Fig. 6. Overview of the event handling process for a simple IMP program.</figcaption></figure>

Reads from top to bottom; for legend and notations, please see Section 4.1.
control flow combinator trees and sound leaves. This means relating return values and events (as in `ret-and` and `do-and` in Section 3) through Galois connections. This new predicate is initially true as a result of the mirroring between `ast2itree` and `ast2aflow`, and the soundness of the user's `ret-and` and `do-and` arguments. It is preserved through each round of handling by a combination of preserving the combinator tree (discussed just below) and the soundness of each abstract event handler w.r.t. its concrete counterpart (7). Since event handlers implement the analyses for language features, this is where the core of the analyzer is proven.

At the unfolding stage, we finally argue that the abstract interpretation algorithms used to analyze control flow are correct, which implies sound. The definitions and proofs for both predicates are properly detailed in Section 6.

## 4.2 Preserving the Combinator Tree During Event Handling

So far in this section, we have assumed that event handling did not affect the nested structure of control flow combators in either program. Upon closer inspection however, it is not obvious that this tree should remain the same when handling events. There are two reasons for this:

(1) Some monadic handlers add new data (e.g. global state) in the concrete program. Since the abstract program explores multiple (often independent) paths of the concrete program, new data in the abstract program should flow along the control flow paths of the analyzed program, not the control flow paths of the analysis algorithms.

(2) Some monadic handlers simply add new control flow (e.g. failure) in the concrete program. In this case, it is not even immediately clear whether a loop that might fail midway still counts as a loop and whether the associated algorithms implemented in the abstract program correctly account for this option.

To illustrate (1), consider the C-like expression `(condition) ? (true-value) : (false-value)`, which evaluates to `true-value` when the `condition` is true, and `false-value` otherwise. Assuming that the condition is not statically determined, the abstract program will compute an approximation of both options using a joining “algorithm”, along these lines:

$$ 
\begin{align*}
t &\leftarrow [true-value] ; ; \\
f &\leftarrow [false-value] ; ; \\
ret (t \sqcup f).
\end{align*}
$$

Notice how this models two different paths of the concrete program, but in terms of the abstract program it is simply a normal sequence. If we tried to implement this computation as a naive monadic sequence and use the normal state monad handler w.r.t. some handler `h` to add some global state, we would get the following incorrect data flow:

$$ 
\begin{align*}
s &\mapsto (s', t) \quad \leftarrow \text{handle\_state } h [true-value] s ; ; \\
(s'', f) &\leftarrow \text{handle\_state } h [false-value] s' ; ; \\
ret (s'', t \sqcup f),
\end{align*}
$$

The final state `s'` of the `true` branch is used as the initial state for evaluating the `false` branch (instead of `s`) and ignored in the join (instead of being joined with `s''`). This happens because adding state to a joining algorithm for analyzing pure programs does not result in a joining algorithm for analyzing stateful programs. As a result, event handling in the abstract world requires each algorithm (and therefore each abstract control flow combinator) to change in subtle ways to account for new monadic effects.

Reason (2) ends up being more of the same-mutating control flow algorithms through event handling requires algorithmic changes that differ from naive monadic handling. Although as a rule
<figure><img src="image_4.png" /><figcaption>Fig. 7. Diagram representation of parameterized seq and do-loop combinators.</figcaption></figure>

of thumb, changes needed to account for new control flow paths are usually more complicated than those needed to account for new data flow paths.

Our solution to this issue is to use parameterized control flow structures that always account for the possibility of added state and non-local exits; they generalize, in a way, the usual notion of what a “conditional” or a “loop” is. Figure 7 shows our models for two of these structures, the sequence and do-loop. The left column shows the control flow paths in the concrete version of each combinator, including early exits for failure. The right column shows the data flow of the interpretation algorithm that approximates it (do-loop’s back edge is a fixpoint approximation). Each of the computations relies on *parameters* which are pure computations used to selectively enable or disable features of the algorithm.

Focusing on the concrete sequence first (top left), we see that the sequence point after the execution of $p_1$ runs a “step” function that determines whether a non-local exit was taken (labeled ERROR), in which case the program exits immediately, returning a value of type $U_2$. Otherwise, the second half of $p_2$ is run (path labeled OK) with the normal return value of $p_1$ of type $T_1$.

Writing the step function requires some introspection into the return type $U_1$ of $p_1$; in practice $U_1$ type is isomorphic to $T_1 + U_2$ at any given time, but interestingly it is not practical to *define* it that way. This is because during handling $T_1$, $U_1$ and $U_2$ change (e.g. into pairs when handling into the state monad, some of them into options when handling in the failure monad), so the isomorphism also changes, and it is significantly easier to factor that into the step function than
<figure><img src="image_5.png" /><figcaption>Fig. 8. Definition of the `aflow` monad (). Type# is a Type equipped with a Lattice.</figcaption></figure>

to add post-processing into $p_1$. This explains why there are more intermediate types in these combinators than datatypes manipulated by the program.<fnref n="10" />

The concrete do-loop combinator works in much the same way. The loop body first runs on the initial value `init` of the loop variable, and returns a result of type $U_1$ indicating either a successful step or a non-local exit. This time the successful value of type $U_2$ comes equipped with a true-ness predicate (from a `BooleanDomain` class not discussed in detail here) which drives the decision to keep looping or return. As before, $U_2$ is basically isomorphic to `Value * (T + U_3)` but defining it this way creates issues during handling, so a new introspection function `dist` is introduced.

The abstract combinators replicate much of this formalism, but are generally more linear because they analyze all paths. For instance, the abstract sequence combinator evaluates both the `ERROR` and `OK` paths and joins the result with the `merge` function at the end. `merge` is essentially a lattice join except that it avoids joining when the error path is statically not taken, as conservatively evaluated by the `may_exit` function. (It is not enough to rely on join-with-$\perp$ identities here because the error path can carry extra data such as global states.) The abstract do-loop combinator follows the same logic, but this time, a mixture of joining and widening is used to implement the fixpoint approximation scheme. Note how $U_1$ is introspected as a *product* `Value*T*U_3` since the abstract interpreter looks at all paths.

Having these parameterized flow combinators allows us to perform event handling by adding new monadic effects into the abstract program simply by reinstantiating them all with updated parameters. These combinators are the least modular part of the design as they need to deal with every monadic effect supported by the source language. Still, many control flow mechanisms derive from simple primitives (non-local exits for instance model `abort()` but also `break`, `continue`, the first halves of `goto` and `try-catch`, and so on), making this a worthwhile endeavor in our view.

# 5 IMPLEMENTING THE ABSTRACT INTERPRETER

We now describe the programmatic side of the library in more detail. We first introduce the `aflow` monad, and its primitive control flow structures. Then, we discuss the `SurfaceAST` previously shown in Section 3 that enables dual concrete/abstract denotations. Finally, we summarize our supported control flow combinators and their varied implementation methods.

## 5.1 Primitive Control Flow Structures and the `aflow` Monad

The `aflow` monad (defined on Figure 8) is a variant of the freer monad with built-in control flow structures. Its monadic structure is based on the `Ret` constructor and a bind operation that

<footnote n="10">¹⁰As a convention, we name $T_n$ types that contain only material data manipulated by the concrete program (return values, states...) and $U_n$ types that also contain control flow information (here, failures).</footnote>
<table><caption>Fig. 9. Summary of the monads in our implementation.</caption><thead><tr><td>Transformer</td><td>Description</td></tr></thead><tbody><tr><td>stateT s</td><td>stateT s m t = s → m (s * t)<br/>Threads the global state s through computations; each step takes the current state as input and returns an updated one.</td></tr><tr><td>failT</td><td>failT m t = m (option t)<br/>Allows for an early exit (failure path) by returning None.</td></tr><tr><td>stateT# s</td><td>stateT# s m t = s → m (s * t)<br/>Same as stateT.</td></tr><tr><td>failT#</td><td>failT# m t = m (unit# * t)<br/>Adds an extra return value indicating whether the failure path might have been taken, with two possible values: ⊥ (not taken), ()# (maybe taken).</td></tr></tbody></table>

propagates recursively through each constructor's continuation k: _ → aflow E R. We emphasize that this bind represents a sequence in the abstract interpreter which, as discussed in Section 4, does not carry monadic effects during handling—unlike the sequence combinator. This means effects like global states and failure do not propagate automatically in-between the steps of a bind; they are merely reified and passed along, altering computations' type signatures. The Vis constructor provides the freer monad structure and behaves identically to the Vis constructor of itree.

The remaining constructors represent primitive control flow structures, which are the basic building blocks of the abstract versions of the control flow combinators.

* Seq computes the sequence of two computations, accounting for monadic effects added by event handling (and is the abstract sequence combinator from Figure 7);

* Fixpoint computes a post-fixpoint of a loop body (and is the abstract do-loop combinator from Figure 7);

* TailMRec computes a post-fixpoint of a family of mutually-tail-recursive functions.

While we argue that this design of extending the freer monad with control flow structures does not restrict which structures and which effects can be implemented, the obvious limitation of aflow is that its definition is dependent on which primitive control flow structures and which monadic effects are included. However, all combinators expose the same interface and aflow-related functions and theorems are glorified match statements, supporting our claim of generality.

The key feature of aflow is that it implements event handling by using the parameters discussed in Section 4.2. Now, monadic effects in abstract programs are quite different from their counterparts in concrete programs. For instance, failT allows a concrete IMP program to crash. It goes without saying that the corresponding abstract program will not itself crash; instead, it will simply add crashing states to the set of potential final states with a lattice join. In general, monadic handling in the abstract world boils down to two things: (1) using richer lattices to model new effects (e.g., whether the failure path might have been taken), and (2) adding new data-flow paths (e.g., joining potential failure states with the final state).

We implement support for two effects: state (with the state monad transformer) and non-local exits (with the failure monad transformer). The definitions for the traditional concrete transformers and our chosen implementations for the abstract ones are summarized in Figure 9. The handlers for stateT# and failT# are shown on Figure 10—we only show the Ret, Vis and Seq for conciseness and refer the interested reader to the formal development. Most of their work consists in reinstantiating the intermediate types and combinator parameters to enable the effect-internalization features
Handling into the state monad

**Fixpoint** handle_state# (h: E ~ stateT S (aflow F)): aflow E R ~ stateT S (aflow F) R :=
**fun** p s ⇒ **match** p with
| Ret r ⇒ Ret (s, r)
| Vis e k ⇒ ' (s, t) ← h e s;; handle_state# h (k t) s
| @Seq U₁ T₁ U₂ step may_exit merge p₁ p₂ k ⇒
| @Seq (S * U₁) (S * T₁) (S * U₂)
| (fun ' (s, u₁) ⇒ (s, step u₁)) (may_exit ∘ snd)
| (fun b ' (su₁, u₁) ' (su₂, u₂) ⇒ (if b then su₁ ∪ su₂ else su₂, merge b u₁ u₂))
| (handle_state# h p₁ s)
| (fun ' (s, t₁) ⇒ handle_state# h (p₂ t₁) s)
| (fun ' (s, u₂) ⇒ handle_state# h (k u₂) s)
(* ... *).

Library code

Handling into the failure monad

**Definition** failT_kmerge (et: unit# * T) (p: aflow E (unit# * R)): aflow E (unit# * R) :=
er ← p;; ret (fst et ∪ fst er, snd er).
**Fixpoint** handle_fail# (h: E ~ failT# (aflow F)): aflow E R → failT# (aflow F) R := fun p ⇒
**match** p with
| Ret r ⇒ Ret (⊥, r)
| Vis e k ⇒ et ← h e;; failT_kmerge et (handle_fail# h (k (snd ex)))
| @Seq U₁ T₁ U₂ step may_exit merge p₁ p₂ k ⇒
| @Seq (unit# * U₁) T₁ (unit# * U₂)
| (step ∘ snd) (fun ' (et, t) ⇒ unit#_to_bool et || may_exit t)
| (fun b ' (eu, u) ' (et, t) ⇒ (eu ∪ et, merge (unit#_to_bool eu || b) u t))
| (handle_fail# h p₁)
| (handle_fail# h ∘ p₂)
| (fun et ⇒ failT_kmerge et (handle_fail# h (k (snd et))))
(* ... *).

Algorithm implementations

**Fixpoint** unfold (p: aflow 0 R): itree 0 R :=
**match** p with
| Ret r ⇒ ITree.ret r
| Seq step may_exit merge p1 p2 k ⇒
| u₁ ← unfold p1;;
| u₂ ← unfold (p2 (step u₁));;
| unfold (k (merge (may_exit u₁) u₁ u₂))
| Fixpoint step body init k :=
| pfp_u₁ ← ITree.iter
| (fun t ⇒ u₁ ← unfold (body t));
| let next_t := t ∪ proj3_2 (step u₁) in
| ret (if next_t ⊑? t then inr u₁ else inl (widen t next_t)))
| init;;
| unfold (k (proj3_3 (step pfp_u₁)))
(* ... *).

<caption>Fig. 10. Key operations in aflow: updating parameterized algorithms when handling into the state (ITT) and failure (IT) monads, and their eventual implementations (IT).</caption>

provided by the algorithms. Note that while we focus on the abstract program here, the effect of
handling in the concrete program can also be written as a parameter update, mirroring the process.

A detailed look at the code shows that in the state monad, `handle_state#` on Figure 10, an extra global state `s`: `S` is provided as input and returned along the output. `Vis` supplies it to the event handler, which allows state events to be substituted with pure computations. `Seq`'s introspection functions are updated to indicate that state doesn't cause failure (`may_exit` unchanged) but it is affected if a failure occurs elsewhere (`merge` joins it when `b = true`).
<figure><img src="image_6.png" /><figcaption>Fig. 11. Surface level DSL () for dual concrete/abstract denotations, with notations in comments.</figcaption></figure>

The failure monad, `handle_fail#` on Figure 10, follows a similar structure. In all constructors except `Ret`, the return value `et` of the sub-program is passed to the continuation via the `failT_kmerge` helper, preparing for an eventual merge with the return value `er` of the continuation. This construction encodes the fact that the program may fail either *before* or *during* `k`. Notice, however, that it doesn't add a failure in-between (`k` is always executed). By contrast, a non-local exit is added in `Seq` by programming `may_exit` to recognize the error flag from `p₁` and merge to propagate this information to other transformers.

Of course, these transformations only make sense in light of the associated parameterized algorithms. We first introduced these in the block diagrams of Figure 7, and now conclude their exposition with their implementation at the end of Figure 10. This unfolding step is executed after all events have been handled, such that the event signatures are $E = E^# = \emptyset$ at this point.

## 5.2 The Surface AST and Dual Denotation

As illustrated on Figure 6, the key to our dual denotation scheme is to have the concrete and abstract programs use the same flow combinator tree. Each of these structure can be crafted independently by a user of the library, but this targeted structural similarity invites deriving both programs from a single tree representation. We have briefly seen that representation as the SurfaceAST datatype in Section 3. The Surface AST is mostly a convenience feature wrapping control flow combinators, and its most remarkable feature is its dual concrete/abstract parameterization over events and return values. Its simplified definition is shown on Figure 11.

The type is doubly parameterized (`E`, `E^#` and `R`, `R^#`), selecting one denotation with the boolean `b` through the use of the `csum` type. An easy way to think about this typing is that for a fixed value of `b`, occurrences of `csum` collapse either all to their first argument or all to their second argument.<fnref n="11" />

When passed to `ast2itree` and `ast2aflow`, leaves at `AST_Ret` and `AST'rEvent` convert directly to the `Ret` and `Vis` constructors of `itree` `E` and `aflow` `E^#`, while combinators are substituted with either the concrete or the abstract implementation. Note how the extra parameterization is gone at this level (save for `AST_Do`'s `dist` which enables macros, see below) so the complexity of handling monadic events is hidden from the user.

## 5.3 Implementing Control Flow Combinators

The final piece in our puzzle for implementing the interpreters is defining concrete and abstract flow combinators symmetrically at the top-level. We have delayed this presentation until now

<footnote n="11">¹¹Which means that technically a SurfaceAST is either the concrete or abstract program, not both; but since all constructions generate it for both values of `b` we still treat it as both.</footnote>
<figure><img src="image_7.png" /><figcaption>Fig. 12. Simplified definitions of the seq, do-loop and while-loop combinators.</figcaption></figure>

<table><caption>Fig. 13. Summary of combinators provided by the library.</caption><thead><tr><th>Combinator</th><th>Type</th><th>Description</th></tr></thead><tbody><tr><td>seq</td><td>Primitive</td><td>Pure sequence (with intermediate value)</td></tr><tr><td>do</td><td>Primitive</td><td>Do-loop with return value (fixpoint)</td></tr><tr><td>tailmrec</td><td>Primitive</td><td>Family of mutually-tail-recursive sub-programs</td></tr><tr><td>if</td><td>Specializes tailmrec</td><td>Conditional (with pure condition)</td></tr><tr><td>cfg</td><td>Specializes tailmrec</td><td>Assembly/IR-style Control Flow Graph</td></tr><tr><td>while</td><td>AST macro</td><td>C-style while loop (with effectful condition)</td></tr></tbody></table>

because we actually provide multiple mechanisms for defining combinators, as a way to balance flexibility (in using accurate abstract interpretation algorithms) with proof effort. Figure 13 shows the six combinators that we implement, which can be categorized into three tiers.

*Primitive control flow structures:* Some control flow combinators are provided directly with an ITree implementation and a primitive structure in aflow; these are seq, do and tailmrec. The definitions for seq and do, which implement the diagrams from Figure 7, are given at the start of Figure 12. The concrete version in each is similar to the standard implementation discussed in
Section 2, but with state and failure parameterized. The abstract version is just the corresponding `aflow` constructor, since it's only substituted with an implementation after handling events.

*Specializations of primitive structures:* The tailmrec combinator is fairly expressive, as it captures all kinds of intra-functional control flow that traditionally gets compiled down to CFGs in IRs, such as C-style conditions, loops, switch statements, etc. We define cfg as an instance of it (essentially just encoding the fact that there is only one entry point) and if as the restricted case of a tailmrec with two non-recursive subprograms.

Naturally, the abstract interpretation of an `if` statement is more accurately computed with a simple join than with tailmrec's general fixpoint approximation scheme. The library allows us to specify and use such a specialized algorithm once it is proven correct. This allows for maintaining accuracy with significantly less proof effort than defining a new primitive structure because `if` gets tailmrec's preservation-through-handling properties for free.

*AST macros:* Finally, we provide a while-loop combinator as a “macro” in the surface AST. `while(c)` unfolds to the equivalent of `if(c) { do b while(c) }` before the concrete and abstract interpreters are extracted. The code for this as well as the unit-version used by IMP in Section 3 is shown at the end of Figure 12. With this method, no specialized algorithm can be used for interpreting the loop in the abstract program, but no proofs are required at all.

# 6 LAYERED PROOF OF SOUNDNESS

After having defined a concrete and an abstract interpreter together, we finally turn out attention to the formal certification of the latter w.r.t. the former.

The core property to prove is the following sound predicate, which captures the soundness condition for programs with empty event signatures. It describes the traditional intuition that any value that the concrete program could return must be covered through the Galois connection by the abstract value returned by the unfolded abstract program:

$$ 
\begin{array}{l}
\text{sound } (p : \text{itree } \emptyset \text{ R}) (p^\# : \text{aflow } \emptyset \text{ R}^\#) \triangleq \\
\quad \forall r r^\#, p \text{ returns } r \rightarrow \\
\quad \phantom{\forall r r^\#, p \text{ returns }} \text{unfold } p^\# \text{ returns } r^\# \rightarrow \\
\quad \phantom{\forall r r^\#, p \text{ returns }} r \in r^\#,
\end{array}
$$

where “`p` returns `r`” expresses that the computation terminates with value `r`.<fnref n="12" /> Note that in case of computations obtained by the construction of monadic interpreters, the return types `R` and `R#` include at this stage global states and failure flags, so every feature of the source language is covered by this single statement.

The top-level theorem we establish then simply states that the interpreters are related by sound after supplying suitable initial states. For instance for IMP (ⓘ):

$$ \forall (c : \mathbb{C}) s s^\#, s \in s^\# \rightarrow \text{sound} (\text{imp\_interp } c s) (\text{eval}^\# c s^\#). $$

We go over the entire proof process in the next section and clarify which proof obligations need to be provided by the user in Section 6.2.

## 6.1 Generic Meta-Theory

As discussed in Section 4, most of the proof of soundness is conducted over a stronger notion of soundness that tracks the control flow tree, and is only lowered down to sound once all events have

<footnote n="12">¹²The signatures being empty, there is at most one such leaf.</footnote>
been interpreted. We call this tree-aware predicate *flow soundness* (), and define it with

$$
\text{sound}' (p : \text{itree E R}) (p' : \text{aflow E}^\# \text{R}^\#) : \text{Prop}
$$

which asserts that *p* and *p'* have identical tree structure, and:

* Pairs of leaves (pure value and events) are related by appropriate Galois connections;

* Pairs of nodes (always the concrete and abstract version of the same combinator) use abstract parameters that correctly approximate the concrete parameters. The definition of “sound parameters” depends on each algorithm and we shall treat it as opaque here.

This predicate is initially true for nodes because `ast2itree` and `ast2aflow` produce identical trees with sound initial parameters, and it is also true for leaves if the user's denotation supplies appropriate values and events in the `ret-and` and `do-and` statements.

*Preserving sound' during handling.* The key property of sound' is that it is preserved during event handling as long as related concrete/abstract events get handled into sound sub-programs. This requirement is, of course, where the soundness of the abstract analysis for each language feature comes into play: the user needs to prove that their abstract handlers are sound. The predicate for this varies slightly depending on the monad transformer at hand, but is otherwise straightforward; it is shown below. The predicate `evl_in` is the Galois connection for events.

**Definition** `handlerSoundIdT` (h: E ↛ itree F) (h#: E# ↛ aflow F#) :=
∀ U U# (e: E U) (e#: E# U#), `evl_in` e e# → `sound'` (h e) (h# e#).

**Definition** `handlerSoundStateT` (h: E ↛ `stateT S` (itree F)) (h#: E# ↛ `stateT S#` (aflow F#)) :=
∀ U U# (e: E U) (e#: E# U#) (s: S) (s#: S#),
`evl_in` e e# → s s# → `sound'` (h e s) (h# e# s#).

**Definition** `handlerSound_failT` (h: E ↛ `failT (itree F)`) (h#: E# ↛ `failT# (aflow F#)`) :=
∀ U U# (e: E U) (e#: E# U#), `evl_in` e e# → `sound'` (h e) (h# e#).

The library provides theorems for lifting this handler soundness from individual events to
entire programs, thus accomplishing the preservation step shown by double arrows in the middle
column of Figure 6. There is one such theorem per monad transformer in which we handle events,
named `handlingSound_*`. Their proofs mostly express that the process of updating control flow
combinators' parameters during event handling maintains their (opaque) soundness property. As
an example, the preservation theorem for the state monad ( applicative monad) is stated as

**Lemma** `handlingSound_stateT`
(h: E ↛ `stateT S` (itree F)) (h#: E# ↛ `stateT S#` (aflow F#))
(t: itree E R) (f#: aflow E# R#) s s#:
s ∈ s# →
handler `sound_stateT h h#` →
sound' t f# →
sound' (handle `state h t s`) (handle `state# h# f# s#`).

After handling all events, we finish by unfolding the abstract combiners. It is at this stage that we finally prove that our parameterized abstract interpretation algorithms are sound approximations of their associated concrete control flow structures. These lemmas are slightly intricate to state due to the parameterization, but are otherwise unsurprising. Here is for example the statement for the soundness of the sequence combinator ( applicative monad).

**Lemma** `sound_seq`
step (p₁: itree E U₁) (p₂: T₁ → itree E U₂) (* Concrete parameters *)
step# may_exit# merge# (p₁#: aflow E# u₁#) (p₂#: T₁# → aflow E# U₂#): (* Abstract parameters *)
sound p₁ p₁# →
(∀ t t#, t ∈ t# → sound (p₂ t) (p₂# t#)) →
(* step# , may_exit# , merge# sound w.r.t. step *) →
sound (seq step p₁ p₂) (seq# step# may_exit# merge# p₁# p₂").

These individual combinator theorems culminate in the library-provided `sound_unfold` () theorem:

**Lemma** `sound_unfold`: $\forall (p : itree \emptyset R) (p# : aflow \emptyset R#),$
`sound' p p# -> sound p p#`,

which allows to conclude a formal proof that the abstract program safely approximates its concrete
original, as used at the bottom of Figure 6.

## 6.2 User-Specific Proof Obligations: the Case of IMP

In general for a pair of interpreters defined in the style of Section 3 which use monad transformers
and flow combinators from the library, the user has three kinds of proof obligations.

(1) After providing lattices for abstract types and Galois connections relating them to concrete types, prove related algebraic laws;

(2) Prove that values and events specified in `ret-and` and `do-and` are sound;

(3) Prove that pairs of concrete and abstract handlers are sound.

In IMP's case, the proof effort is particularly minimal because both the interval domain and the
handling of the finite memory storage for variables are also part of basic library utilities. In fact, all
the lemmas proven in the example file `ImpArithFail.v` ( carelessness ) (excluding two boilerplate one-liners)
are listed in Figure 14.

The first step is to establish the soundness of the ASTs. The proof proceeds by induction on
the input program's syntax, but all nodes in the tree are handled by appropriate constructors of
a library-side `SoundAST` predicate. The only non-trivial obligations are for leaves, for which we
apply either `SoundAST_Ret` or `SoundAST`, which reduce to goals about Galois connections. In
`stmt_sound`, these are all closed by `now` or `easy`.

A slightly more exciting proof can be found in the next section showing that the handlers are
sound. This is where most of the analysis for interesting language features is (in this case: arithmetic,
memory, and assertions), and also where our modular proof design shines. We show the proof
for `h_arith_sound`, which after listing the cases for each event reduces to proving that the interval
domain provides sound approximations of integer arithmetic operators. `h assert sound` is similar
but goes through more API layers not shown in this paper. Finally, the memory handler is already
proven sound by a library utility.

We emphasize that the ability to separate these three proofs is a direct benefit of using layered
monadic handling when defining the interpreters. Reusing language components with proven
analyses such as our basic memory handlers, while seemingly innocuous, is also made possible by
the unique modularity of this design.

Which leads into the final theorem, `imp_interp_sound`. This theorem is a direct transcript of
Figure 6 from bottom to top. It goes through every layer by chaining handlers until it reaches the
surface AST, at which point the combination of `stmt_sound` and a library theorem concludes. This
leaves us with an executable reference interpreter and a certified analyzer both derived from a
single denotation of a simple language.

## 6.3 Extending the Library

While we are confident that the theory underlying this paper is expressive enough to cover a wide
range of applications, scaling to realistic languages and analyses will naturally require support for
more control flow combinators and monad transformers.
<figure><img src="image_8.png" /><figcaption>Fig. 14. Proof of soundness of the IMP interpreters defined in Section 3.</figcaption></figure>

While it has not been the focus of this work, new non-relational abstract domains can be added by instantiating the Lattice class and a relevant domain class such as NumericalDomain.

The effort needed to add a new control flow combinator depends on the applicable method, as discussed in Section 5.3. AST macros are free and specializations of existing combinators like tailmrec require limited effort. The only proof obligations in this case are the preservation of the specialized shape (e.g. an if being two non-recursive blocks) during handling, and the soundness of the specialized algorithm (e.g. a join of both branches). Adding a new primitive control flow structure in aflow requires providing an associated parameterized analysis algorithm, which is a non-trivial abstract interpretation question, but otherwise follows a recurring template.

Adding support for a new monad transformer is the most transversal extension, mostly because this requires analysis algorithms to account for any new data- or control-flow from that transformer,
which impacts a lot of code. We believe that this approach can still scale to capture common control flow mechanisms, which are for the most part consistent across large numbers of real-world programming languages.

# 7 RELATED WORK

The seminal paper by Cousot and Cousot [P. Cousot and R. Cousot 1979] has spawned an exception- ally rich literature around the abstract interpretation framework. We refer the interested reader to recent introductory books [P. Cousot 2021; Rival and Yi 2020], and focus on works directly related to the peculiarities of our approach: mechanization and modularity.

*Mechanized abstract interpreters.* The first attempt at mechanizing abstract interpretation in type theory is probably due to Monniaux [Monniaux 1998]. Later on, Pichardie identified during his PhD [Pichardie 2005] that the asymmetric γ-only formulation of the framework was the key to alleviating issues with the non-constructivity of the abstraction function encountered in Monniaux’s approach. We inherit from this design.

The approach eventually culminated in the Verasco [Jourdan et al. 2015] static analyzer: a verified abstract interpreter for the C language combining rich abstract domains to attain an expressiveness sufficient for establishing the absence of undefined behavior in realistic programs. In particular, the analyzer is plugged into CompCert [Leroy 2009] in order to discharge the precondition to its correctness theorem. Verasco supports a notion of modularity essentially orthogonal to the one we propose in the present work: they introduce a system of inter-domain communication based on channels inspired by Astrée [P. Cousot, R. Cousot, et al. 2006]. Extending our work to support such complex abstract domain combinations and scaling from toy languages to realistic analyzers like Verasco is naturally a major perspective. In contrast, we emphasize that Verasco offers none of the core contributions we propose in our approach: no code reuse, no modularity in terms of effects, and a fuel-based analyzer to avoid having to prove the termination of the analyzer.

Skeletal semantics [Bodin et al. 2019] have been leveraged to derive abstract interpreters in a modular fashion that shares commonalities with our approach. Skeletons and their interpretations provide a reusable meta-language in which to code the concrete and abstract semantics of the languages similarly to how we exploit ITrees and aflow with handlers. Despite this superficial similarity, the technical implementations are completely different: in-depth comparison of the two approaches would cause for a fruitful avenue.

Restricting ourselves to γ-only formulations sacrifices part of the abstract interpretation theory: the so-called “computational” style, deriving an abstract interpreter correct by construction from a concrete one. Darais and Van Horn have introduced Constructive Galois Connections [D. Darais and Van Horn 2016; D. C. Darais 2017] to tackle this issue, and formalized their work in Agda.

*Big-step abstract interpreters.* A wide body of work has sought to modularize and improve code reuse in the design and verification of abstract interpreters. Most of them share conceptually with our work the use of a monadic encoding relying on uninterpreted symbols that gets refined in alternate ways.

Bodin et al. [Bodin et al. 2019], previously mentioned, falls into this category and is mechanized in Coq as well. Although Skeleton share some similarities with our approach, the derivation of abstract interpreters from them is essentially ad-hoc. In particular, no principled treatment of effects of the kind our framework offers is supported. Albeit with quite distinct objectives, Boulmé and Maréchal [Boulmé and Maréchal 2019] have also explored the use of monadic semantics to justify the soundness of abstract computations, in the polyhedral domain. Their approach is significantly different to ours: they fix globally the domain, and hence the monad, of interest; they rely on external oracles to embed an impure monad in Coq; they use a form of Dijkstra monad to
characterize abstractly the abstract domain itself. Their work may offer hints to expand ours to richer domains.

Out of the realm of type theory, a wide range of non-mechanized, but paper-proved, frameworks for the modular construction of sound abstract interpreters have been built in general purpose programming languages.

Most notably, Darais et al. [D. Darais, Labich, et al. 2017] adapt Van Horn and Might's so-called *Abstracting Abstract Machine* [Sergey et al. 2013; Van Horn and Might 2010] methodology to build abstract interpreters for higher order languages using definitional interpreters written in a monadic style, rather than low level machines. Written in a general purpose functional language, their approach relies on a representation of the program with open recursion and uninterpreted operations, further refined into concrete, collecting and abstract semantics. In order to ease the construction of such monadic interpreters, Darais et al. have also identified so-called *Galois Transformers* [D. Darais, Might, et al. 2015], well-behaved monad transformers that transport Galois connections and mappings to suitable executable transition systems.

Keidel et al. [Keidel and Erdweg 2019; Keidel, Poulsen, et al. 2018] have proposed a framework for modularizing the concrete and abstract semantics based on arrows [Hughes 2000], a generalization of monads that exposes its input type in addition to its return type. Their work offers a different design point, but shares several objectives with ours. In their formalism, arrows roughly play the role of Skeletons in [Bodin et al. 2019], and of the combination of concrete signatures and *aflow* in ours; in particular, arrows provide them with a first-order language for shared interpreters on which they can reason by structural induction. They show a general theorem decomposing the proof of soundness of an abstract interpreter to a given a shared implementation with arrows, a pair of proven sounds fixpoint operators, and preservation lemmas for each arrow operations. Naturally, in contrast to our work, they do not work in a type theory: their proofs are pen-and-paper, and they use a general purpose programming language, Haskell, as a host language for their implementations.

Studying in further details the relative expressiveness, modularity, and usability of Keidel et al.'s arrows, Bodin et al.'s skeletons, and ours *aflow* would be a valuable endeavor.

Recently, Keidel et al. have considered the modular construction of fix-point algorithms for big-step abstract interpreters [Keidel, Erdweg, and Hombücher 2023]. This endeavor is orthogonal to our contributions and could hopefully be formalized and incorporated.

*Other models for modular semantics and reasoning.* In this work, we use ITrees to implement the concrete interpreter, unfold the abstract interpreter, and reason about semantics. Other works have contributed similar models that are suitable for representing programming languages through modular composition.

Delaware, S. Oliveira, et al.'s *Meta-Theory à la Carte* (MTC) [Delaware, S. Oliveira, et al. 2013] offers an encoding of *Data-Types à la Carte* [Swierstra 2008] in Coq as a means for solving the expression problem. One of the salient common points is MTC's ability to extend the language by adding new constructions without redefining core datatypes, which is designed in a similar way to ITrees' extensible event families. Their implementations differ significantly though: MTC relies on a Mendler encoding of the free algebra and generalization of their universal properties for general recursion, whereas ITrees rely on the freer monad to dodge the positivity issue, and a coinductive model to recover a traced category for recursion. ITrees have put a lot of emphasis into weak bisimilarity to reason about diverging programs, where it is not a concern in MTC.

The follow-up work *Modular Monadic Meta-Theory* (3MT) [Delaware, Keuchel, et al. 2013] goes one step further by adding monadic models of effects to MTC. This is again reminiscent of ITrees, but differs in implementation. ITrees embed effects *via* its free iterative monad structure, as embodied in
the interp function. 3MT, being built on MTC, does so via the free algebra structure, and therefore properly tackles questions related to products of theories—something ITrees handle in a largely ad-hoc way to date.

A completely different approach is Jin et al.'s extension of Coq with family polymorphism [Jin et al. 2023], which introduces a semi-native solution for the Expression Problem (reified into Coq via a plugin). They report briefly at the end on a case study proving an abstract interpreter sound. This case study focuses on exploiting their inheritance-like features for writing an abstract interpreter which is parameterized, as is traditional, over lattice types and transfer functions (still an impressive testament to the expressivity of FPOP). It also appears to allow the abstraction of the integer arithmetic to be defined as an extension of the basic analysis framework, which reduces the complexity of proving the analyzer. The entire hierarchy of the abstract interpreter example remains rooted on an Imp module defining IMP's syntax, which allows for extending IMP but not for taking individual language features of IMP out of this context and reusing them to analyze other languages (which has been the focus of this paper).

# 8 CONCLUSION

We have presented a new way of building modular abstract interpreters in dependent type theory: by language features, following the paradigm of layered monadic interpreters. Having identified unique challenges in handling control flow structures, we adapted the paradigm by using parameterized abstract interpretation algorithms as carriers of monadic effects during the handling process. This enabled us to mirror the process for defining concrete and abstract interpreters, and eventually derive them both from a shared denotation. Additionally, the approach provides the expected benefit of decoupling soundness proofs for each language feature, breaking down the complexity of certification significantly. We have packaged all the contributions presented in this paper into a reusable, freely available as an open-source, Coq library.

While we have demonstrated the viability of the approach with mechanized proofs for two simple languages, IMP and ASM, much work remains to be done to scale it up to realistic languages such as C or LLVM IR, and to realistic analyses such as relational domains and complex fixpoint iteration strategies. Some of these extensions appear orthogonal at first (such as iteration strategies), but others present challenges either in terms of abstract interpretation (e.g. designing parameterized algorithms that support more monadic effects) or in the framework itself (e.g. defining relations between values for an arbitrary language with arbitrary operations). Future work will explore these avenues both theoretically and in implementation.

# DATA-AVAILABILITY STATEMENT

An artifact of this work is available for reproduction on Zenodo [Michelland 2024] and includes source code and dependencies. Source code is further available for reuse through the Git repository at https://gitlab.inria.fr/sebmiche/itree-ai.

# REFERENCES

* Peter Aczel, Jiří Adámek, Stefan Milius, and Jiří Velebil. 2003. "Infinite trees and completely iterative theories: a coalgebraic view." *Theoretical Computer Science*, 300, 1, 1–45. doi: https://doi.org/10.1016/S0304-3975(02)00728-4.

* Martin Bodin, Philippa Gardner, Thomas P. Jensen, and Alan Schmitt. 2019. "Skeletal semantics and their interpretations." *Proc. ACM Program. Lang.*, 3, POPL, 44:1–44:31. doi: 10.1145/3290357.

* Sylvain Boulmé and Alexandre Maréchal. 2019. "Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra." *J. Autom. Reason.*, 62, 4, 505–530. doi: 10.1007/S10817-018-9492-2.

* Venanzio Capretta. July 2005. "General Recursion via Coinductive Types." *Logical Methods in Computer Science*, Volume 1, Issue 2, (July 2005). doi: 10.2168/LMCS-1(2:1)2005.
Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic. 2023. "Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq." *Proc. ACM Program. Lang.*, 7, POPL, 1770–1800. DOI: 10.1145 /3571254.

Agostino Cortesi, Giulia Costantini, and Pietro Ferrara. Sept. 2013. "A Survey on Product Operators in Abstract Interpretation." *Electronic Proceedings in Theoretical Computer Science*, 129, (Sept. 2013). DOI: 10.4204/EPTCS.129.19.

Patrick Cousot. Sept. 2021. *Principles of Abstract Interpretation*. The MIT Press, (Sept. 2021). ISBN: 9780262044905.

Patrick Cousot and Radhia Cousot. 1979. "Systematic design of program analysis frameworks." In: *Principles of programming languages (POPL)*. ACM, 269–282. DOI: 10.1145/567752.567778.

Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. 2006. "Combination of Abstractions in the ASTRÈE Static Analyzer." In: *Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, 11th Asian Computing Science Conference, Tokyo, Japan, December 6-8, 2006, Revised Selected Papers* (Lecture Notes in Computer Science). Ed. by Mitsu Okada and Ichiro Satoh. Vol. 4435. Springer, 272–300. DOI: 10.1007/978-3-540-77505-8\_23.

David Darais, Nicholas Labich, Phúc C. Nguyen, and David Van Horn. Aug. 2017. "Abstracting Definitional Interpreters (Functional Pearl)." *Proc. ACM Program. Lang.*, 1, ICFP, Article 12, (Aug. 2017), 25 pages. DOI: 10.1145/3110256.

David Darais, Matthew Might, and David Van Horn. 2015. "Galois Transformers and Modular Abstract Interpreters: Reusable Metatheory for Program Analysis." In: *Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2015)*. Association for Computing Machinery, Pittsburgh, PA, USA, 552–571. ISBN: 9781450336895. DOI: 10.1145/2814270.2814308.

David Darais and David Van Horn. 2016. "Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory." In: *Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016)*. Association for Computing Machinery, Nara, Japan, 311–324. ISBN: 9781450342193. DOI: 10.1145/2951913.295 1934.

David Charles Darais. 2017. "Mechanizing Abstract Interpretation." Ph.D. Dissertation. University of Maryland, College Park, MD, USA. DOI: 10.13016/M2J96097D.

Benjamin Delaware, Steven Keuchel, Tom Schrijvers, and Bruno CdS Oliveira. 2013. "Modular monadic meta-theory." *ACM SIGPLAN Notices*, 48, 9, 319–330.

Benjamin Delaware, Bruno C d. S. Oliveira, and Tom Schrijvers. 2013. "Meta-theory à la carte." In: *Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages*, 207–218.

Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. 2016. "CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels." In: *Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI'16)*. USENIX Association, Savannah, GA, USA, 653–669. ISBN: 9781931971331. DOI: 10.5555/3026877.3026928.

Peter Hancock and Anton Setzer. 2000. "Interactive Programs in Dependent Type Theory." In: *Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic*. Springer-Verlag, Berlin, Heidelberg, 317–331. ISBN: 3540678956.

John Hughes. May 2000. "Generalising monads to arrows." *Science of Computer Programming*, 37, (May 2000), 67–111. DOI: 10.1016/S0167-6423(99)00023-4.

Ende Jin, Nada Amin, and Yizhou Zhang. 2023. "Extensible metatheory mechanization via family polymorphism." *Proceedings of the ACM on Programming Languages*, 7, PLDI, 1608–1632.

Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. 2015. "A Formally-Verified C Static Analyzer." In: *Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015*. Ed. by Sriram K. Rajamani and David Walker. ACM, 247–259. DOI: 10.1145/2676726.2676966.

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. Dec. 2017. "RustBelt: Securing the Foundations of the Rust Programming Language." *Proc. ACM Program. Lang.*, 2, POPL, Article 66, (Dec. 2017), 34 pages. DOI: 10.1145/3158154.

Sven Keidel and Sebastian Erdweg. Oct. 2019. "Sound and reusable components for abstract interpretation." *Proceedings of the ACM on Programming Languages*, 3, (Oct. 2019), 1–28. DOI: 10.1145/3360602.

Sven Keidel, Sebastian Erdweg, and Tobias Hombücher. Aug. 2023. "Combinator-Based Fixpoint Algorithms for Big-Step Abstract Interpreters." *Proc. ACM Program. Lang.*, 7, ICFP, Article 221, (Aug. 2023), 27 pages. DOI: 10.1145/3607863.

Sven Keidel, Casper Bach Poulsen, and Sebastian Erdweg. July 2018. "Compositional Soundness Proofs of Abstract Interpreters." *Proc. ACM Program. Lang.*, 2, ICFP, Article 72, (July 2018), 26 pages. DOI: 10.1145/3236767.

Oleg Kiselyov and Hiromi Ishii. Aug. 2015. "Freer Monads, More Extensible Effects." *SIGPLAN Not.*, 50, 12, (Aug. 2015), 94–105. DOI: 10.1145/2887747.2804319.

Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic. 2019. "From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server." In: *Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs* (CPP 2019). Association for Computing Machinery, Cascais, Portugal, 234–248. ISBN: 9781450362221. DOI: 10.1145/3293880.3294106.
Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. "CakeML: A Verified Implementation of ML." In: *Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages* (POPL '14). Association for Computing Machinery, San Diego, California, USA, 179-191. ISBN: 9781450325448. DOI: 10.1145/2535838.2535841.

Xavier Leroy. 2009. "Formal verification of a realistic compiler." *Commun. ACM*, 52, 7, 107-115. DOI: 10.1145/1538788.1538814.

Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, and Steve Zdancewic. 2022. "C4: verified transactional objects." *Proc. ACM Program. Lang.*, 6, OOPSLA1, 1-31. DOI: 10.1145/3527324.

Thomas Letan, Yann Régis-Gianas, Pierre Chiflier, and Guillaume Hiet. July 2018. "Modular Verification of Programs with Effects and Effect Handlers in Coq." In: *FM 2018 - 22nd International Symposium on Formal Methods* (LNCS). Vol. 10951. Springer, Oxford, United Kingdom, (July 2018), 338-354. DOI: 10.1007/978-3-319-95582-7_20.

Conor McBride. 2015. "Turing-Completeness Totally Free." In: *Mathematics of Program Construction*. Ed. by Ralf Hinze and Janis Voigtländer. Springer International Publishing, Cham, 257-275. ISBN: 978-3-319-19797-5.

[SW] Sébastien Michelland, *Replication package for article: Abstract Interpreters: a Monadic Approach to Modular Verification* June 2024. DOI: 10.5281/zenodo.11470739, URI: https://doi.org/10.5281/zenodo.11470739.

David Monniaux. 1998. "Réalisation mécanisée d'interpréteurs abstraits." Master's thesis. Université Paris 7.

David Pichardie. 2005. "Interprétation abstraite en logique intuitionniste : extraction d'analyseurs Java certifiés." Ph.D. Dissertation. Université Rennes 1. In french.

Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hrițcu, Vilhelm Sjöberg, and Brent Yorgey. May 2018. *Logical Foundations*. Software Foundations series, volume 1. Version 5.5. http://www.cis.upenn.edu/~bcpierce/sf. Electronic textbook, (May 2018).

Maciej Piróg and Jeremy Gibbons. 2014. "The coinductive resumption monad." *Electronic notes in theoretical computer science*, 308, 273-288.

Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock, et al.. 2019. "QED at large: A survey of engineering of formally verified software." *Foundations and Trends*® in *Programming Languages*, 5, 2-3, 102-281.

Xavier Rival and Kwangkeun Yi. Feb. 2020. *Introduction to Static Analysis: An Abstract Interpretation Perspective*. The MIT Press, (Feb. 2020). ISBN: 9780262043410.

Grigore Rosu and Traian-Florin Serbanuta. 2010. "An overview of the K semantic framework." *J. Log. Algebraic Methods Program.*, 79, 6, 397-434. DOI: 10.1016/j.jlap.2010.03.012.

Ilya Sergey, Dominique Devriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, and Frank Piessens. June 2013. "Monadic Abstract Interpreters." In: vol. 48. (June 2013), 399-410. DOI: 10.1145/2491956.2491979.

Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, and Steve Zdancewic. 2023. "Semantics for Noninterference with Interaction Trees (Artifact)." *Dagstuhl Artifacts Ser.*, 9, 2, 06:1-06:2. DOI: 10.4230/DARTS.9.2.6.

Wouter Swierstra. 2008. "Data Types à la Carte." *Journal of Functional Programming*, 18, 4, 423-436.

David Van Horn and Matthew Might. Sept. 2010. "Abstracting Abstract Machines." *SIGPLAN Not.*, 45, 9, (Sept. 2010), 51-62. DOI: 10.1145/1932681.1863553.

Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. 2020. "Interaction Trees." *Proceedings of the ACM on Programming Languages*, 4, POPL. DOI: 10.1145/3371119.

Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, and Steve Zdancewic. Aug. 2021. "Modular, Compositional, and Executable Formal Semantics for LLVM IR." *Proc. ACM Program. Lang.*, 5, ICFP, Article 67, (Aug. 2021), 30 pages. DOI: 10.1145/3473572.

Hengchu Zhang et al.. 2021. "Verifying an HTTP Key-Value Server with Interaction Trees and VST." In: *12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)* (LIPIcs). Ed. by Liron Cohen and Cezary Kaliszyk. Vol. 193. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 32:1-32:19. DOI: 10.4230/LIPIcs.ITP.2021.32.

Jianzhou Zhao, Santosh Nagarakatte, Milo M.K. Martin, and Steve Zdancewic. Jan. 2012. "Formalizing the LLVM Intermediate Representation for Verified Program Transformations." *SIGPLAN Not.*, 47, 1, (Jan. 2012), 427-440. DOI: 10.1145/2103621.2103709.

Received 2024-02-28; accepted 2024-06-18