Scaling Up Mechanized Proof Automation for
Small-step Semantics

Sandrine Blazy¹[0000-0002-0189-0223], Alain Delaët¹[0000-1111-2222-3333], and Denis Merigoux²[0000-0003-2247-0938]

¹ Inria, Univ Rennes, CNRS, IRISA

² Inria Paris

**Keywords:** operational semantics, mechanized proofs, proof assistant

**Abstract.** Verifying the correctness of a program using an interactive proof assistant involves first defining in the proof assistant the semantics of the programming language used to write the program. Once mechanized, the semantics of the programming language serves as the basis for the whole proof development, as it is referred by all subsequent theorems. Traditionally, the semantic judgments are mechanized using recursive inductive predicates, matching the pen-and-paper inference rules of operational semantics. However, the shape of these judgments may make proof engineering and maintenance tedious, requiring complex proof automation frameworks.

In this paper, we highlight a different style of writing and mechanizing semantics, based on continuations. We show that continuation-based small-step semantics interacts better with basic proof automation tactics than the traditional operational style, and as such allows for scaling up more efficiently the mechanized proof development. After detailing the inner workings of the interactions between the semantic style and proof automation of common theorems, we perform a case study for the medium-sized Catala domain-specific programming language. All of our examples and case studies are mechanized using the Rocq proof assistant, and our development is available as a supplementary material.

# 1 Introduction

Proof assistants have come a long way in the last twenty years, to the point where software as complex as realistic compilers have been proven correct. A verified piece of software consists of the software itself, that runs outside of the proof tool (as any other software), together with a machine-checked proof that the software is correct with respect to its specification. When the software implements a program transformation (e.g., a compilation pass), the specification expresses its semantic preservation, thus involving the formal semantics of the underlying programming languages.

Semantic reasoning on realistic languages generates large proofs and requires a proof tool to handle the whole proof. Automatic proof tools discharge logical
formulas to logic solvers, but they are not adapted to prove the correctness of so-
phisticated program transformations operating over realistic languages. Indeed,
to be able to reason on the semantics, it is necessary to somehow deeply embed
it inside the proof tool. Hence, proofs about semantics require tricky reasoning,
especially when the proof requires inductive reasoning on a new data structure
yet to be found. For this reason, proof assistants (a.k.a. interactive proof tools)
are rather used in these situations (mainly to follow the laws of mathematical
logic) where user interaction is still needed to decide on what to reason. The
price to pay is that they require to write elementary proof steps (called *tactics*),
which makes the proofs difficult to maintain. What is tricky is to define and
prove the semantic invariants, as this may necessitate inventing data structures
for the sole purpose of the proof.

Moreover, developing a verified piece of software requires both programming
the software using the programming language of the proof assistant so that it
runs efficiently on real programs, and defining a semantic model together with
abstractions to reason about, in order to conduct the proof. This software/proof
co-design is a real scientific challenge. Indeed, although these two objectives are
closely related (as the proof directly uses the software code, in addition to the
semantic notions on which the reasoning is done), they are also sometimes antag-
onistic (e.g., the proof needs to compute additional data structures facilitating
the reasoning but slowing down the execution of the compiled programs, or the
software uses less efficient functional data structures).

Nearly all theorems of a mechanized development for verified software will
refer back to the semantics of the language, whether one is building a verified
compiler [4, 6, 17], a verified abstract interpreter [15], or a verified bug-finder [8].
As such, the encoding of the language semantics inside a proof assistant is a
critical and central software component of the mechanized development. From a
software engineering point of view, the design patterns and coding style of the
language semantics as a program in the proof assistant heavily influence the rest
of the mechanized development, as it is a direct dependency to everything else.

Mechanized semantic reasoning relies on operational semantics. The correct-
ness theorem of a program transformation (from a source program to a target
program) states that any execution of one of the programs is simulated by the
execution of the other one, while ensuring some invariants. The standard way to
prove these simulations is to reason inductively on both semantics, which can be
more or less mechanized, depending on the language under scrutiny. Conversely,
finding these invariants can be tricky and more difficult to mechanize.

More generally, the standard methodology to develop a verified piece of software proceeds as follows.

1. Define the involved programming languages, namely the inference rules of their semantics, specified as a relation between a syntactic element and semantic states.

2. Program the piece of software mainly within the proof assistant, and within the semantic model of the language.
3. State the main correctness theorem (related to the program and the semantics) and start the proof to reason inductively on the semantics.

4. Continue the proof. For each inductive case, take into account the program transformation and compute intermediate results (which may require further case reasoning) in order to eliminate spurious proof goals and to simplify the remaining ones. Conclude each case by applying the adequate semantic rule (e.g., using the tailor-made constructor tactic).

The proof may require to iterate steps 3 and 4, in order to define new semantic invariants and intermediate lemmas. Moreover, it may be useful to debug the semantics, which requires replaying the proof many times over. There are other reasons why proofs need to be replayed (and updated): firstly, programming languages evolve to satisfy users needs, and secondly, new intermediate representations may be added to facilitate the proofs (and split them in smaller and more maintainable pieces).

Furthermore, automating these proofs is not a simple task, as the sequence of elementary proof steps is not straightforward; it depends on the properties to prove, on the need to combine inductive and case reasonings. If elementary proof steps are well understood, as they correspond to specific tactics (mainly induction or case reasoning, inversion used to invert hypotheses, or simpl used to apply a computation and simplify a formula), there is a number of ways of combining them. This raises the question of what can we do to improve proof engineering and especially proof automation, which is the subject of this paper.

This subject arose during the development of a new verified compiler for the Catala domain-specific programming language [22]. Catala is a language designed for situations where a given set of laws or regulations has to be turned into computer code for automatic enforcement. In practice, this situation concerns mostly tax or social benefits computations, which have been digitalized by government agencies in developed countries for several decades. A software program computing taxes automatically from an income declaration must take into account all possible income and tax schemes, and return the legally correct result for all of them. These strong requirements make these sometimes thousands-of-lines-of-code-long programs [23] hard to write and maintain, as the source of truth for their behavior is determined by legal interpretation performed by government lawyers.

To ensure that the decisions and specifications of these government lawyers are accurately and faithfully transcribed into the computer code, Catala has a set of syntactic and semantic features that facilitates the review of the program source code by lawyers. First, Catala allows for literate programming, locally linking each snippet of computer code to the article of statutes or regulations that specifies it. Second, Catala's semantic is based on default logic [18], a logic that matches how the law lays out its instructions for how to compute things. Because tax- and social-benefits-computing programs are critical for the smooth operation of States, a high level of assurance is also required from the Catala compiler that translates the source Catala code to target programming languages such as C or Python.
Catala's semantics and compilation will thus be used as an empirical evalua-
tion of the proof engineering and automation techniques discussed in this paper.
While Catala is not as complex as real-world general-purpose languages like C [4],
it is based on an fully-fledged simply typed λ-calculus with classical extensions.
Moreover, the reduction order of some Catala language constructs is non-trivial
and requires a small-step operational semantics to be specified precisely. Unless
noted otherwise, all results presented in this paper have been mechanically ver-
ified using the Rocq proof assistant. The complete development is available as a
supplementary material. Specifically, we claim the following novel contributions.

**Semantics styles:** We mechanize a continuation-based semantics of a λ-calculus, and prove its equivalence to a traditional small-step semantics.

**Semantics and tactics:** We explain in detail the different interactions between
basic proof automation tactics and semantic judgments, depending on the
style of semantics.

**Proof engineering:** We rely heavily on state-of-the-art proof automation tech-
niques and demonstrate that they are critical to scale up our formalization.

**Application:** We illustrate how our findings scale on the proof of a novel com-
pilation pass for the Catala domain-specific programming language.

This paper is organized as follows. First, Section 2 presents two styles of
small-step semantics for a call-by-value λ-calculus. Then, Section 3 details how
these styles, once mechanized, interact with the basic blocks of proof automa-
tion in a proof assistant. Finally, Section 4 illustrates how continuation-based
small-step semantics allows for a better scaling up of proofs in mechanized de-
velopments. It introduces λ<sup>δ</sup>, a new mechanized semantics for Catala's core in-
termediate representation, the default calculus, as well as the proofs of various
theorems around λ<sup>δ</sup>, including the correctness of a non-trivial compilation pass.
Related work is discussed in Section 5, followed by conclusions.

## 2 Mechanizing Small-step Semantics: Choose Your Style

There are many ways to mechanize programming language semantics inside a
proof assistant. Coupled with the criticality of the semantics as a central proof
component, this choice of semantic styles makes for a hard decision for the proof
engineer in the mechanized development. Indeed, the decision to go for a certain
semantic style will determine the shape and details of all future proofs in their
development, as well as how easy they will be to write, debug and repair.

Admittedly, the syntax of terms quite naturally maps to an inductive type
inside the proof assistant, without a lot of room for user fantasy. But the typing
and reduction judgments can be mechanized in different forms. Indeed, one can
chose to mechanize typing and reduction as total or partial functions over terms,
thus building an executable typer or interpreter for the language. But this en-
coding differs quite significantly from the way programming languages semantics
are written on paper, with standard inference rules.
As the semantics encoding is part of the trusted computing base of the mechanized development, it is better for the encoding to match closely the pen-and-paper rules for better human review [20, Section 1.2.1]. Also, since functions have to be proven total, encoding semantics as functions quickly becomes cumbersome. Hence, the recommended way [24, 28] to mechanize typing and reduction judgments is to define them as inductive types, with a family of constructors, where each constructor corresponds to a different pen-and-paper inference rule. This also ensures that the case analysis inside the proof assistant will closely follow the case analysis of pen-and-paper proofs, familiar to the human user.

But even when encoding the judgments of a language semantics as an inductive type with a family of rules-constructors, the user is still left with some degrees of freedom. They correspond to degrees of freedom that also exist when defining pen-and-paper semantics. For instance, one can define a small-step or a big-step semantics. The small-step and big-step versions of the semantics of a language are equivalent in the sense where they yield the same final outcome, but they will be expressed with very different rules, and be mechanized by different inductive types. In this paper, as discussed earlier, we will only focus on small-step semantics, which constrains this freedom. But additionally, there is another style dichotomy for language semantics authors to choose from when writing their semantics. We will name the two styles of this dichotomy as “traditional small-step semantics” and “continuation-based small-step semantics”.

This section presents these different ways of defining equivalent small-step semantics, both on paper and inside the proof assistant. The traditional small-step semantics should feel familiar as it represents the most taught and presented style in the field. On the contrary, the continuation-based semantics can feel more artificial and verbose, while very precise and exhaustive. Why bother with the continuation-based small-step semantic style if it is not standard? We will answer this question in the next section, where we dive deep into the issues of proof automation and proof repair, and compare the effect of the two semantic styles. Note that CompCert itself has been using the continuation-based small-step semantics style [4]. But for now, we will present the two different styles with a toy language that will serve as a running example for this section and the next: a simply-typed λ-calculus (though we will mostly focus on its reduction rather than its typing), augmented with a standard if-then-else construct and boolean values. Its syntax is defined as follows.

<table><tr><td>Values</td><td>v ::= λ x. t<br>| true | false</td><td>lambda<br>boolean</td></tr><tr><td>Terms</td><td>t ::= x | v<br>| t t<br>| if t then t else t</td><td>variable, value<br>application<br>conditional</td></tr></table>

Now, let us move to the semantics, defined by the judgment $t \rightarrow t'$ for traditional small-step semantics, and $s \rightsquigarrow s'$ for continuation-based semantics.
the argument term. The context reduction rule uses this function to state that if a term reduces, then any context applied to this term also reduces.

Both variants of the traditional small-step semantics share key characteristics. First, they feature a recursive judgment, with recursive rules at least for the contextual reduction. Second, this recursiveness brings extra premisses to the rules (to state that sub-terms reduce); they have an important effect when manipulating the inference rules in the context of a meta-theoretical proof.

Indeed, suppose we want to know which rules can apply to a term *t* to determine *t'* such that *t* —> *t'*. This is a very frequent pattern in proofs (see next section). We case analyse each rule to determine whether it can apply or not. The syntactical shape of *t* allows us to discard a lot of rules that cannot apply. However, suppose *t* is *if true then t₂ else t₃*. Then, we can narrow down eligible rules to IF-TRUE, but also the condition-related contextual rule (IF-COND or CONTEXT). This rule might apply because we cannot rule out immediately that the premise *true* —> *t'* might hold for some *t'*. Of course, we can further deduce that there is no *t'* such that *true* —> *t'*, but this requires an extra proof step. Hence, the determination of which rule can be applied for a given term requires more than a purely syntactic analysis of the term; it also requires a recursive examination of which rules apply or not for its sub-terms. While this extra consideration is not an issue for pen-and-paper proofs, it matters when conducting mechanized proofs, as explained later.

## 2.2 Continuation-based Small-step Semantics

Some operational semantics rely more than others on an abstract (or virtual) machine to represent the current state of the execution. In our presentation above of a call-by-value simply-typed λ-calculus that relies on substitution, no such machine was needed: the information about the state of the reduction is purely contained within the syntax of terms. However, it is very common when defining operational semantics to include in the reduction judgment some sort of context or environment with its own syntactic category, distinct from terms. For instance, an environment mapping variables to values when the reduction is call-by-name. Pushing this idea further, the reduction judgment sometimes features complex syntactic artefacts that encode information about the state of the reduction that cannot be contained syntactically in the terms.

For instance, as we will proceed below, one can encode in the reduction state a notion of continuation, that tells the reduction routine where to resume when the current sub-term has been fully reduced. Encoding the notion of continuation as a syntactic artifact in the reduction state is consensually less readable and elegant than encoding it as a recursive premise of the reduction judgment, as we did above. While traditional small-step semantics is thus a more human-readable and agreeable form of semantics presentation, ideally suited to a pen-and-paper presentation and reviewing, we will later argue that it may not be the ideal way to encode a semantics inside a mechanized proof development.

For now, we present an alternative version of the semantics of our running example language, using continuations encoded as an abstract machine, that we
call “continuation-based small-step semantics”. This presentation is inspired by recent works [16, Section 5], where an extra typographical effort tries to balance the dryness of the abstract machine characteristics.

The judgment of the continuation-based semantics is $s \rightsquigarrow s'$, where states $s$ and $s'$ augment the term $t$ being reduced with extra information about the state of its reduction: $s$ is written $S(t, \kappa, \sigma)$ when reducing $t$, and $C(v, \kappa, \sigma)$ when the reduction returned value $v$. The semantics uses a variable environment $\sigma$ rather than substitutions, to map variables to values. The continuation $\kappa$ represents the remaining reductions that need to be done once $t$ is reduced; it is a stack of control units, each control unit roughly standing for the location where a sub-term is being reduced in a larger term. In this sense, each control unit corresponds to a case of the reduction context $C$. For instance, $k_{\text{if}}(t, t)$ corresponds to `if ... then ... else ... t`, $k_{\text{app}}(t)$ corresponds to `t`, and $k_{\text{clo}}(x, t, \sigma)$ corresponds to $(\lambda x. t)$. The states as thus defined as follows.

<table><tr><td>Control unit</td><td>k ::= k<sub>app</sub>(t)<br>| k<sub>clo</sub>(x, t, σ)<br>| k<sub>ret</sub>(σ)<br>| k<sub>if</sub>(t, t)</td><td>function application<br>function abstraction<br>function return<br>reduction of the if condition</td></tr><tr><td>Continuation</td><td>κ ::= k<sup>*</sup></td><td>continuation stack</td></tr><tr><td>Environment</td><td>σ ::= x ↦ v, σ |</td><td>map from variables to values</td></tr><tr><td>State</td><td>s ::= S(e, κ, σ)<br>| C(v, κ, σ)</td><td>reduction state<br>continuation state</td></tr></table>

However, handling function abstraction and application requires some additional syntactic artifacts. First, $k_{\text{ret}}(\sigma)$ corresponds to the reduction of the body of a function before returning its results. Because we use a variable environment $\sigma$, we need to know when we exit or enter a function application to update $\sigma$ accordingly. Second, the closure $<\lambda x. t \lhd \sigma>$ represents an intermediate computation artifact corresponding to a $\lambda$-term that carries its environment of free variables. Closures replace $\lambda$-terms as function values, hence the syntax of terms and values change:

<table><tr><td>Values</td><td>v ::= &lt; λ x. t &lhd σ &gt;<br>| true | false</td><td>closure<br>boolean</td></tr><tr><td>Terms</td><td>t ::= x | v<br>| t t | λ x. t<br>| if t then t else t</td><td>variable, value<br>λ-calculus<br>conditional</td></tr></table>

The semantic rules of the continuation-based semantics are defined as follows. Let us start by the reduction rules for functions. COMP-VAR computes the value of a free variable by querying it in $\sigma$. FOC-APP focuses the computation of $t_1 t_2$ on the function $t_1$, storing the function argument $t_2$ in the continuation stack $\kappa$. When the reduction of $t_1$ finishes, it should return a $\lambda$-term that is computed into a closure $<\lambda x. t_{\text{cl}} \lhd \sigma_{\text{cl}}>$ by rule COMP-ABS. The rule RES-APP then resumes the reduction of the whole function application by popping the last control unit
off the stack, and switching it to the next control unit corresponding to the reduction of the function argument. When the reduction of the function argument finishes and returns value $v$, the RES-BETA rule performs the equivalent of the substitution by pushing the mapping $x \mapsto v$ to the environment $\sigma$ and resumes the reduction of the function body. Finally, rule COMP-RET computes the final result $v$ of the function application.

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

From the description of these rules, three categories emerge. First, some rules compute a result: they step to a state $C$. Second, some rules focus the reduction onto a sub-term: they reduce a state $S$ to another state $S$. Third, some rules resume the computation after a result was returned: they reduce a state $C$ into a state $S$. By switching alternatively between $S$ states and $C$ states, the rules carefully decompose the reduction step in a very predictable manner for every semantic feature. Similarly, here are the reduction rules for conditionals.

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

These rules are already much more readable, mainly because they do not have to deal with updating $\sigma$. FOC-IF corresponds to the IF-COND rule of the traditional small-step semantics, while COMP-IF-TRUE and COMP-IF-FALSE correspond to IF-TRUE and IF-FALSE. COMP-VAL is a bookkeeping rule that signals a term has fully reduced to a (boolean) value, switch the state from $S$ to $C$.

The first thing to note about the continuation-based small-step semantics is that its rules are not recursive. Indeed, the recursiveness and the contextual reduction premises are now all taken into account by the continuation stack. As to encoding inside a proof assistant, it is fairly straightforward. Semantic states are simply defined, while the judgment can still be mechanized with an inductive family of constructors with as many inductive cases as semantic rules. This absence of recursion eliminates almost all premises from the reduction rules, except in places where they are semantically needed like COMPVAR and accessing the variable environment correctly.

Second, continuation-based small-step semantics add many extra reduction steps, as we have added more rules. Let us illustrate this by comparing the reductions from a state $S(\mathbf{if} \ \mathbf{true} \ \mathbf{then} \ t_1 \ \mathbf{else} \ t_2, \nil, \nil)$, corresponding to the term $\mathbf{if} \ \mathbf{true} \ \mathbf{then} \ t_1 \ \mathbf{else} \ t_2$. For each step, we can reconstruct from the current state a whole term by applying all control units in the continuation
stack. Here is the result of this reconstruction for each reduction step. So, it takes four steps to perform what the IF-TRUE rule does in one step for the previous semantics. This extra steps can appear artificial, but it reflects a key characteristic of the continuation-based small-step semantics.

As explained previously, in the traditional small-step semantics, determining which rule can be applied for a given term *t* requires more than a purely syntactic analysis of *t*; it also requires a recursive examination of which rules apply or not for some sub-terms of *t*. However, thanks to continuations, this extra requirement disappears: the syntactic shape of the initial state completely and uniquely determines which rule to apply. In a nutshell, switching from a traditional small-step semantics to a continuation-based small-step semantics adds new inference rules and reduction steps, but the structure of the reduction rules is harmonized and more regular, leading to a better automatic handling in proof assistants. In the next section, we will expand on this claim and examine how it impacts a mechanized development inside a proof assistant.

<table><thead><tr><th>Reduction state</th><th>Reconstructed term</th></tr></thead><tbody><tr><td>S(<span style="color:red;">if true then t<sub>1</sub> else t<sub>2</sub></span>, [], [])</td><td>if true then t<sub>1</sub> else t<sub>2</sub></td></tr><tr><td>≈> S(true, [k<sub>if</sub>(t<sub>1</sub>, t<sub>2</sub>)], [])</td><td>if true then t<sub>1</sub> else t<sub>2</sub></td></tr><tr><td>≈> C(true, [k<sub>if</sub>(t<sub>1</sub>, t<sub>2</sub>)], [])</td><td>if true then t<sub>1</sub> else t<sub>2</sub></td></tr><tr><td>≈> S(t<sub>1</sub>, [], [])</td><td>t<sub>1</sub></td></tr></tbody></table>

# 3 Proof Ergonomy and Repair: Comparing Styles

Now that we have described the continuation-based small-step semantics, this section explains why it is easier to manipulate within a formal development than traditional small-step semantics. The root argument is that the rules of continuation-based small-step semantics do not have recursive premises applying the reduction judgment on sub-terms, as continuations are used to encode these premises. For this reason, the behavior of common tactics such as **constructor** and **inversion** becomes much simpler. Thus, continuation-based small-step semantics enables us to automate large parts of our proofs, as hinted by a recent presentation by one of the authors of CompCert [3].

## 3.1 The Effect of Semantic Style on Common Proof Patterns

This section dives into the mechanics of proofs in both semantic styles, in order to highlight precisely the root causes and the particular setting that makes continuation-based semantics better for proof automation. The absence of recursive premises in one style leads to three differences when developing mechanized proofs in both styles. Firstly, when making hypothesis more precise: applying the **inversion** tactic on a traditional small-step semantics judgment inevitably
leads to the introduction of new, incoherent proof goals. Secondly, when applying
the **constructor** tactic on a traditional small-step semantics judgment where
multiple constructors could (syntactically) be applied may lead to false proof
goals. This makes automation harder as we need to know which rule leads into
false proof goals. Thirdly, structural induction on traditional small-step seman-
tics may not be powerful enough. While this also holds for continuation-based
small-step semantics, it is possible to reason inductively on continuations $\kappa$ in-
stead, which is easily tractable. We will detail these three claims in the following.
While our work is built around the Rocq proof assistant, similar problems arise
in other implementations of type theory.

*Inverting judgments.* The goal of the **inversion** tactic is to find the premises of a judgment that is an hypothesis of another judgment. Inverting judgments is a stable of proofs about semantics to infer more information. For instance, if we know that $C(\mathbf{false}, k_{\mathbf{if}}(t_a, t_b) :: \kappa, \sigma) \rightsquigarrow s'$, we can deduce that $s' = S(t_b, \kappa, \sigma)$. Indeed, this hypothesis can only be derived from rule **COMP**-**FALSE**. The **inversion** tactic works by syntactically unifying the hypothesis with every constructor of the type of the hypothesis. In our example, only one constructor can be unified, but we may have multiple constructors with successful unifications. In these cases, the **inversion** tactic generates a new proof goal for each unification, which may trigger further inversions of generated hypotheses.

In particular, applying **inversion** to a traditional small-step semantics hy-
pothesis may result in additional proof goals that are irrelevant: while one ap-
plies **inversion** with a specific rule in mind, multiple other rules that also syn-
tactically unify might be returned by the proof assistant. For instance, given
**if true then t₁ else t₂ → t'**, an **inversion** will generate two new proof
goals. One instantiates the **IF-COND** rule with **true** and creates a new hypothesis
**true → t'**. The other corresponds to the rule **IF-TRUE**. The rule **IF-FALSE** will
fail to unify, hence it will not generate a third proof goal. While two proof goals
were generated, only the second one is relevant. Indeed, the proof goal corre-
sponding to the rule **IF-COND** is incoherent because the hypothesis **true → t'**
cannot be derived: **true** is a value, and values do not reduce.

Because the **inversion** tactic is a proof staple that is usually applied many
times in a row, and since each application can generate multiple proof goals,
this leads to an exponential growth of the proof cases to analyse manually, and
makes the tactic practically unusable in the context of automation. Admittedly,
it should be possible to modify the reduction rules of a traditional small-step
semantics to avoid this issue by separating syntactically values from terms. How-
ever, this solution is not satisfactory, as values are still syntactically a special
case of terms. In our example, the condition of an **if** is still a term, so the
conclusion of **IF-TRUE** would still be **if (Value true) then t₁ else t₂ → t₁**.
Thus, the syntactic ambiguity when inverting **if (Value true)** would remain
between **IF-TRUE** and **IF-COND**.

Hence, separating syntactically values from terms does not solve the problem
of generating spurious proof goals at inversion time. Alternatively, we could add
a side condition on the rule **IF-COND** requiring that $t_1$ should not be a value.
This side condition can be syntactically checked, and actually solves the problem of generating spurious proof goals. However, adding non-value premises to all contextual reduction rules in a traditional small-step semantics overloads the semantics in a way that is not particularly elegant, and does not fix the other proof automation problems that we present later in this section.

So, instead of fixing this problem with non-value premises in contextual rules, we rather syntactically separate reduction states, namely we distinguish the cases where a sub-term is being reduced from these where this reduction has finished and the whole term now reduces. This is exactly what continuation-based small-step semantics does: given a state $S(t, \cdot, \cdot)$, the sub-term $t$ will be computed, and when a state $C(v, \cdot, \cdot)$ is in continuation mode, the value $v$ corresponding to the sub-term has just been computed.

Thus, applying inversion on a continuation-based small-step semantics hypothesis does not introduce incoherent proof goals. Indeed, given a state, choosing the correct reduction is mainly syntactic as these rules do not have premises requiring a recursive application of the judgment. What makes this possible is the distinction (thanks to continuations) between the start and the end of the reduction of a sub-term.

Let us illustrate how each such reduction choice is unique with the term $t = \text{if true then } t_1 \text{ else } t_2$, when evaluated before the computation of the sub-term `true` from state $S(\text{if true then } t_1 \text{ else } t_2, \emptyset, \emptyset)$. The only applicable rule is FOC-IF. After this, the sub-term is computed, which would correspond to IF-COND in traditional small-step semantics. Finally, the state $C(\text{true}, [k_{\text{if}}(t_1, t_2)], \emptyset)$ is returned, corresponding to `true`. Once again, only rule COMP-IF-TRUE might be applied, corresponding to the rule IF-TRUE. So inverting the two judgments $S(\text{if true then } t_1 \text{ else } t_2, \emptyset, \emptyset) \rightsquigarrow s'$, and then $C(\text{true}, [k_{\text{if}}(t_1, t_2)], \emptyset) \rightsquigarrow s''$ will always constrain $s'$ and $s''$ in a unique proof goal to a particular shape: $s' = S(\text{true}, [k_{\text{if}}(t_1, t_2)], \emptyset)$ and $s'' = S(t_1, \emptyset, \emptyset)$. This helps greatly when scaling the proof to more complex constructs, as we will see in Section 4.

The unique syntactic result of the inversion of a judgment instance can be viewed as a meta-property of the judgment itself. This meta-property can be checked empirically by trying to invert every possible instance of the judgment, and assert that at most one unique proof goal is generated. Alternatively, this meta-property could be expressed as a MetaCoq [32] statement and proved accordingly. We leave the illustration of this MetaCoq case study as future work.

*Introducing judgments.* The goal of the constructor tactic is to prove a conclusion defined inductively by applying of its constructors. A common pattern where this tactic is used is when trying to prove that a reduction judgment holds given some hypotheses. Specifically, given an evaluation step, we need to figure out its outcome, which can be achieved using existential variables, noted $?t$, that represent unknown terms that need to be instantiated in order to solve the proof goal. So, we place an existential variable $?t$ on the right-hand side of a reduction and apply constructor to instantiate $?t$ when it finds a fitting constructor. For instance, the rule IF-TRUE matches the term `if true then t_1 else t_2 -- ?t` and will instantiate $?t$ as $t_1$. Namely, the constructor tactic sequentially applies
each of the conclusion's type constructors, stopping at the first applicable one. The selected constructor's arguments are then instantiated as new proof goals. If no constructor can be applied, then the tactic fails.

Contrary to continuation-based small-step semantics, using `constructor` on a traditional small-step semantics judgment can lead to the introduction of unprovable proof goals. For example, suppose we use the `constructor` tactic to solve the goal `if true then t₁ else t₂ → ?t`. Two rules may be applied, `IF-COND` and `IF-TRUE`. Applying `IF-COND` will generate `?t'` (and the sub-goal `true → ?t'`) and instantiate `?t` as `if ?t' then t₁ else t₂`. We are left with the goal `if true then t₁ else t₂ → if ?t' then t₁ else t₂`, which holds only if the additional goal `true → ?t'` can be solved. This cannot happen as `true` is a value. So, `constructor` can pick from two matching constructors but only one allows us to conclude the proof. More generally, the previous fix (of adding non-value premises to contextual reduction rules) will lead to more instances of the problem of picking the right match for `constructor`. There are two workarounds to overcome this `constructor` problem, but neither is satisfactory.

The first one is to reorder the constructors when defining the semantics, so that the most precise rule is tested before the more general one (e.g., writing `IF-COND` after `IF-TRUE` and `IF-FALSE`). Sadly, this approach is very brittle. The order of constructors should not significantly modify the proof script for this statement, as this hinders proof repair [30, Chap. 4]. The second workaround is to explicitly write which constructor is the correct one, instead of using `constructor`, but this leads to long and manual proofs. This is not what we want, as our goal is to automate as much of the proof process as possible.

In contrast, in continuation-based small-step semantics, `constructor` almost always either fails, or selects the only applicable constructor, without introducing unprovable goals. Still, some rules have premises: for instance, the check whether a variable belongs to the current environment. But, they do not include any recursive reference to the reduction, contrary to the contextual reduction rules in traditional small-step semantics. It is thus possible to handle their proof with automation. Furthermore, we know that at most one rule is applicable syntactically without considering the premises. Therefore, if a premise is unsolvable, the reduction itself is unsolvable. So, `constructor` does not introduce any unprovable goal. Overall, when used with continuation-based small-step semantics, the `constructor` tactic becomes a very powerful yet simple proof automation tool.

***Induction Principles.*** The last advantage of continuations is the improved handling of induction principles, which is paramount in semantic reasoning.

First, let us describe inductive reasoning on traditional small-step semantics. When an evaluation step is recursive, one may need the induction hypothesis $H_{ind}$ to concern the reduction of a deeper sub-term than the direct sub-terms of the term at hand. For example, proving a predicate $P$ by induction on $(t_1 \ t_2) \ t_3 \rightarrow (t'_1 \ t_2) \ t_3$ may require $P$ to hold on $t_1 \rightarrow t'_1$. Obtaining $H_{ind}$ on deeper sub-terms is challenging because the automatically generated induction principle for $\rightarrow$ is shallow: it only provides the induction hypothesis for direct sub-terms. Hence, it would merely state that $P$ holds inductively for
$t_1 t_2 \rightarrow t'_1 t_2$. To address this issue, it is common to use one of two approaches, depending on the context: either perform induction on a well-founded measure, or hand-write a custom induction principle tailored to the proof's requirements.

In paper-and-pen proofs, the induction is often performed on the size of the judgment itself. Transposing this into proof assistants requires reflection capabilities on the terms, which in turn requires the proof to operate at a meta-level. This increases the complexity of the proof engineering effort, making it an undesirable strategy to adopt. Performing induction on the size of terms is the most common solution, as it only requires defining a decreasing measure on terms. Such proofs generally start by performing induction on the size of terms and use **inversion** on the induction hypothesis featuring the reduction judgment. However, this adds an indirection between the induction and the reduction judgment, increasing the size of predicates and intermediate hypotheses. Moreover, it also requires using **inversion**, and thus, issues related to **inversion** may arise again. Finally, each application of the induction hypothesis requires to check that the size is indeed smaller, which may not always be the case. For instance, the **β-REDUCTION** rule might increase the size of the terms, requiring the measure to take into account the effects of yet-to-be-performed substitutions.

The other workaround is to write a custom induction principle, but this is error-prone. It requires a deep understanding of the proof before writing it, and it is difficult to maintain when repairing proofs [30], since it is the synchronized combination of the induction principle and the induction predicate that makes the proof go through. Since the induction principles are not yet defined at this stage, they must be written manually, often requiring low-level tactics or basic lemmas. As a result, any update of the semantics will require tedious manual restating and reproving of the induction principles.

By contrast, continuation-based small-step semantics handles induction principles differently. Since the reduction judgment is not recursive, inductive reasoning boils down to case analysis of the semantics. Interestingly, we found that properties such as determinism, progress, and even the correctness of a translation pass require no more than a case analysis of the semantic judgment as opposed to a proper recursive induction.

Nevertheless, a stronger truly recursive induction principle is needed to prove some more complex theorems. To illustrate what happens with continuation-based small-step semantics, we use as an example the theorem stating the equivalence between our traditional small-step semantics and continuation-based small-step semantics. It uses a correspondence between traditional small-step semantics and continuation-based small-step semantics based on the notion of reconstructed terms, informally defined in Section 2.2. We write $s \sim t$ if the term reconstruction of continuation-based semantic state $s$ matches $t$. More precisely, we show that if $t$ reduces to $t'$ in traditional small-step semantics, then any state $s$ equivalent to $t$ in the sense of term reconstruction reduces to $s'$ in continuation-based small-step semantics through multiple steps, where $s' \sim t'$.
**Theorem 1 (Simulation of continuation-based small-step semantics by traditional small-step semantics).** Let $t \rightarrow t'$, and $s \sim t$. Then, there exists $s'$ such that both $s \rightsquigarrow^* s'$ and $s' \sim t'$.

The key lemma for this proof states that if we step from $s_1$ to $s_2$ in the continuation-based semantics, then the same step, but with an extended continuation stack, holds as well. To express appending an extra continuation stack $\kappa$ to a state $s$, we use the same notation $s ++ \kappa$ as for concatenating lists. For example, if $s$ is $S(t, \kappa, \sigma)$, then $s ++ \kappa_{\text{extra}}$ becomes $S(t, \kappa ++ \kappa_{\text{extra}}, \sigma)$.

**Lemma 1 (Contextual reduction lemma).** Let $s_1, s_2$ be states and $\kappa_{\text{extra}}$ a continuation stack. If $s_1 \rightsquigarrow s_2$, then $s_1 ++ \kappa_{\text{extra}} \rightsquigarrow s_2 ++ \kappa_{\text{extra}}$.

Writing such a compact and powerful lemma in traditional small-step semantics is not possible. Instead, an equivalent formulation for just two levels of contextual reduction (two control units in $\kappa_{\text{extra}}$) would require a number of distinct lemmas quadratic in the number of contextual reduction rules. However, note that if the traditional small-step semantics uses an evaluation context with a unified contextual reduction rule, then it is possible to write and prove a lemma equivalent to Lemma 1. However, the traditional small-step semantics with an evaluation context and unified contextual reduction rule still suffers from issues related to the inversion and constructor tactics, as well as the generation of induction principles.

Let us now examine one case of the proof of Theorem 1 to illustrate why induction on continuations is necessary, and why Lemma 1 is key. The global proof outline of Theorem 1 is as follows: first perform induction on the continuation stack of $s$, followed by a case analysis on both $t \rightarrow t'$ and $s \sim t$. Indeed, an induction on $\rightsquigarrow$ is not possible, since the judgment is not recursive; only the continuation stack is. Alternatively, we could perform induction on $\rightarrow$, but the proof would fail when trying to match the reduction step in $\rightarrow$ with those in $\rightsquigarrow$ in cases involving function returns (corresponding to the $k_{\text{ret}}(\sigma)$ control unit), since $\rightsquigarrow$ has more reduction steps than $\rightarrow$ in this case.

Hence, we follow our proposed global proof outline and start by performing induction on the continuation stack of $s$. In the resulting case analysis on both $t \rightarrow t'$ and $s \sim t$, there is a case of interest to us, where we need a deeper induction hypothesis: the contextual reduction of function application APP-ARG: $t_2 \rightarrow t'_2 \Rightarrow t = (\lambda x. t_1) t_2 \rightarrow t' = (\lambda x. t_1) t'_2$, together with the state $s = C(< \lambda x. t_1 \lhd \sigma_1 >, [k_{\text{app}}(t_2)], \sigma)$. On the side of the continuation-based small-step semantics, we apply RES-APP to step from $s$ to $s' = S(t_2, [k_{\text{clo}}(x, t_1, \sigma_1)], \sigma)$. Here, we cannot apply the induction hypothesis to $s'$, since it has the same continuation stack size as the initial state $s$. However, we can apply the induction hypothesis on $S(t_2, [], \sigma)$, since $S(t_2, [], \sigma) \sim t_2$ and $t_2 \rightarrow t'_2$. This results in a new state $s'_2$, where $S(t_2, [], \sigma) \rightsquigarrow^* s'_2$ and $s'_2 \sim t'_2$.

Finally, since $s'_2 \sim t'_2$, we deduce that $s'_2 ++ [k_{\text{clo}}(x, t_1, \sigma_1)] \sim v_1 t'_2$, and by Lemma 1, state that $s = S(t_2, [k_{\text{clo}}(x, t_1, \sigma_1)], \sigma) = S(t_2, [], \sigma) ++ [k_{\text{clo}}(x, t_1, \sigma_1)]$, and $s \rightsquigarrow^* s'$ with $s' = s'_2 ++ [k_{\text{clo}}(x, t_1, \sigma_1)]$, thus concluding the proof. The remaining cases of the global proof are dealt with similar reasoning.
Induction on continuation stacks, as seen here, is particularly convenient for
handling complex reductions. Thanks to Lemma 1, we can remove the continua-
tion stacks of terms, apply the induction hypothesis with an empty continuation
stack (where it always holds), prove the expected property, and stack back the
continuations to generalize our result. While most simpler proofs, such as those
for properties like determinism and progress (see below), can typically be han-
dled with straightforward case analysis, this method of performing induction on
the continuation stack scales remarkably for the more complex proofs involving
continuation-based small-step semantics, independently of the level of sub-term
inspection required to complete the proof.

## 3.2 Comparing Semantic Styles: Proving Determinism and Progress

We previously outlined the key differences between both semantics in their in-
teraction with the building blocks of inductive predicate mechanized handling:
the inversion and constructor tactics, as well as the generated induction
principles. In this section, we show that choosing a semantic style with a good
interaction towards these building blocks allows for easy-access powerful proof
automation. This automation enhances the user experience for the proof of meta-
properties about the language and its compilation like determinism or typing
safety. Furthermore, our proof automation techniques are resilient to semantic
changes, overall facilitating proof maintenance and proof repair.

*Minimizing proof maintenance.* Most proofs involving semantics can be effec-
tively structured using the following generic proof outline. Typically, the proof
begins with an induction on one hypothesis. Then, an inversion on the remaining
judgments extracts the necessary information, and the proof proceeds by case
analysis on the many cases generated. Each case requires applying appropriate
constructor tactics and leveraging hand-crafted lemmas. This last phase of the
proof is the most time consuming, as finding the right lemmas and the correct
constructor to apply can be challenging. Hence, one way to mitigate the com-
plexity of the proof is to limit the number of cases where manual intervention is
needed, by automating away the handling of a maximum number of cases.

Having a consistent proof outline during proof maintenance greatly simplifies
the process. A study on the activity of Rocq proof engineers [31] shows that most
of the maintenance time is spent updating definitions like syntax, reductions, and
typing rules, followed by repairing the impacted proofs. By keeping the proof
outline unchanged during such modifications, only the specific cases affected
by the changes need to be updated. Moreover, it is possible that the newly
introduced cases are already covered by the automation tactic in place. This
ensures that properties proofs often do not need to be adjusted, allowing the
engineer to proceed to the next properties with minimal disruption.

Although heavier automation techniques exist, they often require a deep un-
derstanding of the proof assistant's inner workings to debug complex tactics,
which can make maintenance challenging [31]. Instead, we focus on small-scale
automation that operates effectively with a well-suited semantic style. This approach works better with the continuation-based small-step style of semantics compared to traditional small-step semantics, as explained in the last section, due to its efficient interaction with constructor and inversion tactics. Now, we will show how to leverage these benefits in two case studies, where we strive to simplify proofs and reduce their complexity.

*Determinism.* Our first case study concerns the proof of the reduction determinism in both semantic styles. This property only involves the reduction judgment, and states that if $t \to t_1$ and $t \to t_2$, then $t_1 = t_2$. Its proof is simpler in continuation-based small-step semantics thanks to its interaction with the inversion tactic. Indeed, while our proof outline follows the same structures as detailed earlier – an induction on the first reduction and an inversion on the second reduction – the number of cases left to handle manually afterwards differs. In traditional small-step semantics, there are 8 cases related to the application, and 5 more for the if-then-else, as the inversion tactic fails to discard irrelevant contextual rules application of the reduction judgment. This means that the number of cases is quadratic in the number of judgments for each language construct. In contrast, when using continuations, the proof size is constant: basic automation solves all cases. In a more complex setting, we believe that the remaining cases to prove determinism will involve language features where determinism is actually difficult to prove.

In Section 3.1, we described a variant of traditional small-step semantics with extra premises on contextual reduction rules specifying that the sub-terms are not values. It better interacts with the inversion tactic; in the determinism proof the number of cases to handle manually is linear, one for each contextual reduction. Hence for this variant, the complexity of the proof falls between that of traditional small-step semantics and continuation-based small-step semantics.

*Progress.* Our second case study is the proof of progress for the reduction judgment in both semantic styles. Progress ensures that terms either take a reduction step or are already values. Unlike determinism, progress requires not just the reduction judgment but also involves typing. As a result, to express progress for continuation-based small-step semantics, we need to extend the typing of terms $(\Gamma \vdash_t t : \tau)$ to include the typing of states.

To achieve this, we introduce a new typing judgment for continuation stacks: $\Gamma_1 \Rightarrow \Gamma_2 \vdash_c \kappa : \tau_1 \Rightarrow \tau_2$. Recall that continuation stacks are basically contexts with a hole; by filling the hole with a sub-term, we can reconstruct a bigger term. Hence, the typing judgment for $\kappa$ states supposes that the hole in $\kappa$ has type $\tau_1$ under environment $\Gamma_1$, such that the term after reconstruction from $\kappa$ has type $\tau_2$ under $\Gamma_2$. From the typing judgment on continuation stacks, we can naturally deduce a typing judgment on reduction states: $\Gamma \vdash_s s : \tau$. We refer the reader to the mechanized development in the supplementary material for the full definitions of the specific judgments.

With this typing judgment, the progress property in traditional small-step semantics states that if $t$ is a term such that $\vdash_t t : \tau$, then either there exists
a term $t'$ such that $t \to t'$, or $t$ is a value. For continuation-based small-step semantics, it applies to states: if a state $s$ is such that $\Gamma \vdash_s s : \tau$, then either there exists a state $s'$ such that $s \rightsquigarrow s'$, or $s$ is a value state, meaning it has the shape $C(\cdot, \llbracket, \cdot)$. Note that the environment is absent from the traditional small-step semantics progress statement, but is present in the continuation-based small-step semantics one, as it is present in the semantics, hence we need to ensure the type of each variable present in $\sigma$ has the correct type. So, the requirement that the term is closed for traditional small-step semantics is not required for continuation-based small-step semantics. The proof follows the generic proof outline for both semantics.

For traditional small-step semantics, we first perform induction on the typing judgment. Then, constructor handles cases where reduction occurs, and syntactic checks identify when the term is a value. After basic automation, three main cases remain: one for variables (easily handled since the term is closed) and one each for applications and conditionals. In these cases, we instantiate the induction hypothesis and invert the typing judgments. This leads to 8 cases, which are solved using the same constructor tactic as earlier. The number of cases scales linearly with the number of constructors, but the proof is brittle: changes to the order constructors or a missing case analysis can break the proof automation as mentioned previously, leading to expensive manual intervention.

For continuation-based small-step semantics, due to the different typing judgments and state shapes, we start by doing a precise case analysis on the form of the state: either $S(t, \kappa, \sigma)$, where a term is being evaluated, or $C(v, \kappa, \sigma)$, where a value has been computed and the continuation stack is being processed. In the case of $S(t, \kappa, \sigma)$, we further perform case analysis on the structure of $t$ to handle the different constructors. For $C(v, \kappa, \sigma)$, we examine the possible shapes of $v$ and the first control unit in the continuation stack $\kappa$, which corresponds to specific evaluation steps (such as function application or if-condition evaluation). After this case analysis, we invert the typing judgments involving constructors. Since each language construct typically corresponds to one typing judgment, applying tactics such as inversion does not introduce spurious goals. This step is automated using a hand-crafted tactic in Rocq, which we reuse in other contexts.

After inversion, we are left with 10 cases, most of which are resolved using the same automation tactics as in the traditional small-step semantics proof: use constructor for cases where reduction occurs, and syntactic check when the state is a value state. In contrast to traditional small-step semantics, there is a single case left, related to the COMP-VAR rule and requires a lemma: if a variable is associated to a type in the typing environment, then that variable is also associated to a value in the environment. Overall, the proof is a lot simpler in continuation-based small-step semantics once the typing judgment has been correctly extended. Moreover, if we forget to perform case analysis (e.g., on the condition of an if), additional goals are simply added without introducing inconsistencies contrary to the traditional small-step semantics proof. Hence, using continuation-based small-step semantics is more robust.
To conclude this comparison, maintaining typing definitions and theorems requires effort linear to the number of language constructs. However, continuation-based small-step semantics is more robust: while traditional small-step semantics can break easily with changes to the order of constructors or missing inductions, continuation-based small-step semantics manages changes better through its handling of continuations, supported by custom tactics. This makes these semantics more resilient and easier to maintain when proving progress.

# 4 Scaling Up Proof Automation: Application to Catala

This section shows how the proof engineering differences between semantic styles shown so far scale up with Catala [22], a more realistic language targeted for industrial usage inside government agencies, for computer programs in charge of estimating the amount of taxes and social benefits. These programs have to follow a legal specification, and Catala has special semantic features to account for the peculiar logical structure of the law. Here, the context and details of the Catala compilation chain are irrelevant, as we focus on the formal semantics of the core intermediate representation of Catala, the default calculus.

More specifically, we introduce a novel mechanization of Catala's default calculus in Rocq, that we call $\lambda^\delta$. Its syntax is presented in Figure 1: it is a standard $\lambda$-calculus, enriched with a “default term” with shape $\langle t^* | t : - t \rangle$. For instance, $\langle t_{ex1}, t_{ex2} | t_{just} : - t_{cons} \rangle$ reads as a default term with two exceptions $t_{ex1}$ and $t_{ex2}$, that defaults to a base case consequence $t_{cons}$ when the base case justification $t_{just}$ is true. This logical structure posits that exceptional cases should apply first, and only by default the base case should apply. For instance, suppose two free variables $x, y: \texttt{bool}$ and consider the default terms

$$a = \langle | x : - \langle 1 \rangle \rangle, b = \langle | y : - \langle 2 \rangle \rangle \text{ and } c = \langle a, b | \texttt{true} : - \langle 0 \rangle \rangle.$$

$a$ and $b$ do not have any exceptions (left of “$|$”), hence they behave as conditionals on $x$ and $y$: if $x$ is true, then $a = \langle 1 \rangle$, otherwise $a = \emptyset$ (nothing applies), and likewise for $b$. Note that the consequence of a default term must have a default type $\langle \texttt{integer} \rangle$, while $1$ has type $\texttt{integer}$. Transforming $1$ into a pure default term $\langle 1 \rangle$ solves this problem. However, $c$ is a default term with two exceptions, $a$ and $b$. If one of the exceptions applies (for instance, $a \neq \emptyset$), then it is returned (and $c = a$). If none apply, then $c = \langle 0 \rangle$ because the justification of the default term (left of “$:$”) is true. If $a$ and $b$ apply ($x = y = \texttt{true}$), then there is a conflict of exceptions and the computation crashes, returning $c = \texttt{\textbf{\texttt{?}}}$.

The default term and its semantics have proved empirically powerful enough to accurately formalize the entirety of the real-world French housing benefits [21]. In practice and in the Catala computer code, $a$, $b$ and $c$ are partial definitions of the value of a legal variable, that are activated by a boolean justification and related to each other by exceptional and base case relationships.

A traditional small-step semantics was presented previously for the default calculus in [22, Figure 6]. Its judgment is $t_1 \rightarrow t_2$, and selected rules for default terms are presented in Figure 2. For $\lambda^\delta$, we modified the semantics in the four
<table><caption>Fig. 1: Syntax of $\lambda^\delta$. $t^*$ denotes a list of terms.</caption><tr><td>Types</td><td>τ ::= <b>bool</b> | <b>integer</b> | <b>unit</b><br>| τ → τ<br>| &lt;τ&gt;<br>| <b>option</b> τ</td><td>atomic types<br>function type<br>default type<br>option type</td></tr><tr><td>Values</td><td>v ::= &lt;v&gt;<br>| n ∈ N<br>| <b>true</b> | <b>false</b><br>| &lt;λ x. t | σ &gt;<br>| <b>None</b> | <b>Some</b> v</td><td>pure default<br>integer<br>boolean<br>closure<br>option</td></tr><tr><td>Closure env.</td><td>σ ::= (x ↦ v)*</td><td>environment</td></tr><tr><td>Typing env.</td><td>Γ ::= (x ↦ τ)*</td><td>environment</td></tr><tr><td>Term</td><td>t ::= x | v<br>| t <b>op</b> t | <b>fold</b> t t* t<br>| λ x. t | t t<br>| <b>match</b> t <b>with</b> | None → t | Some x → t</td><td>variable, value<br>binary operator, fold<br>λ-calculus<br>match<br>None | Some t<br>default term</td></tr><tr><td>Default</td><td>d ::= &lt;t*| t :- t&gt;<br>| &lt;t&gt;<br>| <b>crash_if_empty</b> t<br>| ⊕<br>| Ø</td><td>default term<br>pure default term<br>crash if empty<br>conflict error term<br>empty error term</td></tr></table>

following ways (see the detailed rules in the Rocq development). Firstly, we extend the semantics with classic rules for integer values, arithmetic operators, optional constructors and pattern matching, and a fold operator. Secondly, we changed the computation of defaults. Consider $d = \langle \emptyset, t_2 | t_{\text{just}} :- t_{\text{cons}} \rangle$, where the first exception evaluates to $\emptyset$. In the original semantics, when $t_2 \rightarrow t'_2$, then $d$ reduces to $\langle \emptyset, t'_2 | t_{\text{just}} :- t_{\text{cons}} \rangle$. Note that $\emptyset$ exceptions are kept while evaluating the subsequent ones. These extra $\emptyset$ were an unpleasant source of bookkeeping for little semantic added value, since they do not influence the final value. Hence, we decided to tweak the default evaluation which leads to $d$ reducing to $\langle t_2 | t_{\text{just}} :- t_{\text{cons}} \rangle$.

The third modification concerns $\lambda$ values. In $\lambda$-calculus, $\lambda$ terms are values. However, because we included a $< \lambda x. t | \sigma >$ closure value in $\lambda^\delta$, we use it in our small-step semantics. Concretely, $\lambda x. t \rightarrow < \lambda x. t | [] >$ and function application requires $< \lambda x. t | [] >$ to reduce. Note the empty closure environment, reflecting our use of substitution in this semantics. The last modification concerns the typing of defaults and the introduction of a pure default term, that better tracks by typing the program points where $\emptyset$ might appear and propagate.
<figure><img src="image_3.png" /><figcaption>Fig. 2: Selected reduction rules for $\lambda^{\delta}$</figcaption></figure>

## 4.1 Proof Engineering with $\lambda^{\delta}$

Because $\lambda^{\delta}$ is closer to a realistic language, the number of cases in the proofs involving the semantics becomes significant. Furthermore, we have proved a number of meta-theoretical theorems about $\lambda^{\delta}$, in both styles: determinism, progress, preservation, equivalence between both semantics. Additionally, we proved in both semantic styles the correctness (semantics preservation) of an optimization pass (noted $\llbracket t \rrbracket$) from $\lambda^{\delta}$ to $\lambda^{\delta}$ aimed at eliminating default terms in favor of matching option-typed terms where the None case represents the $\emptyset$ value. This non-trivial compilation pass is illustrated in Figure 3.

<figure><img src="image_4.png" /><figcaption>Fig. 3: Selected compilation rules for eliminating the default term by using option-typed terms. For the sake of clarity, we use `let ... in`. In our mechanized development, the `let ... in` are inlined as abstractions and application.</figcaption></figure>

To manage all these proofs, we developed automated proof scripts that handle most of the cases. For each one of the main proofs, an automation script is co-developed with it: if the current version of our automated script fails on some individual case, we can check this case, determine which hypothesis or lemma is missing to solve the goal automatically, and add it to our proof script.
To gain a deeper understanding of this methodology, let us revisit the differ-
ent parts of a proof with a proof engineering eye. For instance, for the proof of
equivalence from the traditional small-step semantics to the continuation-based
small-step semantics (Theorem 1), the induction of $t \rightarrow t'$ followed by the in-
version on $s \sim t$ results in approximately 2760 cases. To handle this bulk of
cases, we use proof automation techniques like hypothesis saturation [29, 5.2.1]
to apply induction principles as well as the inversion lemmas. This eliminates
most of the inconsistent goals reducing the number of cases to 344.

An example of an inconsistent proof goal is trying to prove that the term
reconstructed from reduction state $S(t_1, \kappa++[k_{if}(t_2, t_3)], \sigma)$ is of the shape $\lambda x. t'$:
because the last control-unit of the continuation is $k_{if}(t_2, t_3)$, the reconstruction
of the term from the reduction state above necessarily results in a top-level
conditional term, and not a $\lambda$-term. Our tactics detect such discrepancies and
discard these inconsistent goals by contradiction. From the remaining consistent
goals, we apply reduction steps automatically to the remaining cases. This is
where we take the most advantage of the automation-friendliness of continuation-
based small-step semantics. Indeed, writing a meta-interpreter in Ltac [10] is as
simple as : solve[constructor; eauto].

This meta-interpreter performs one reduction step in the proof goal. Switch-
ing to multiple reduction steps is as easy as repeating the tactic above with the
transitivity lemma for reduction. We improve this automation with the ability
to perform total or partial reductions when we only have partial but sufficient
information in our hypotheses. Moreover, we run such a meta-interpreter deep
inside our terms and under quantifiers to avoid introducing extra existential vari-
ables before goal simplification. Automating the solving of any goal involving the
reduction judgment merely becomes a game of expanding the tactic presented
above with the right call to specialized lemmas and simplification repeats.

Overall, we use dozens of these meta-interpreters, each fitting in a few lines of
Ltac. We make sure the subgoals they generate are proved on the spot by an ad-
hoc automation script using [solve[...]]|, so we do not introduce proof goals
that do not have the same shape as the ones we are trying to prove. We see here
that continuation-based small-step semantics allows us to benefit almost for free
from a very powerful meta-interpretation system that vastly automates semantic
proofs. We believe this technique to be the killer application of continuation-
based small-step semantics, for scaling up mechanized proof developments.

Another automation technique on which we rely extensively is a smart in-
version tactic. Indeed, the **inversion** tactic only works on a specific judgment,
meaning that if the proof is updated, then we need to make sure the right judg-
ments are still being inverted. This makes proof repair tedious, especially in
compiler verification proofs where we want to invert all judgments depending
on terms, such as reduction, invariant or typing judgments. What we would
really want is a smart **inversion** tactic for inverting all inductive judgments
that concern a specific term on which we have prior information (e.g. *t* is a
function application). Sadly, if we naively repeat **inversion** on all inductive hy-
potheses, we get a case analysis that loops because of the recursive nature of
judgments in traditional small-step semantics. Our solution is to implement a
smart **inversion** tactic using Ltac2 [27], which greatly improves proof repair
and helps us develop our proofs in an iterative fashion. This smart inversion
only applies **inversion** when the inductive judgment features a term on which
we have prior information (usually, we know the term is in a specific construc-
tor coming from a prior case analysis). For instance it applies **inversion** on
Γ ⊢$_{t}$ t₁ t₂ : τ but not on Γ ⊢$_{t}$ t : τ. We believe the smart inversion trick could
be applied to many Rocq developments.

This automation discipline allows us to quickly deal with the trivial aspects
of proofs, and dive in specifically on remaining goals. While they might be au-
tomatized as well, there is a tradeoff between spending time automatizing them,
or simply treating them manually. Empirically, we find that handling manually
a dozen of case is the best way to balance this tradeoff. Nevertheless, there are
some limitations to our approach. Most importantly, the derivation of induction
principles for our proofs in traditional small-step semantics resists automation,
as we already mentioned in Section 3.1, but also in continuation-based small-step
semantics. Concretely, the presence of both a **list** and an **autosubst** binder in
$\lambda^\delta$'s syntax suffices to break Rocq's automatic induction principle derivation,
which forces us to write the induction principles by hand for some judgments.

## 4.2 Case Study: Proving Equivalence Between Both Styles

After having described our automation discipline in general terms, we present a
proof case study on our most difficult proof, namely the equivalence between both
semantics. The mechanized development of the side that generalizes Theorem 1
relies on the structure of the traditional small-step semantics and counts 606 lines
of specification and 609 lines of proof. Compare this to 213 lines of specification
and 219 lines of proof for the other side, that relies on the structure of the
continuation-based small-step semantics. The case study of first side helped us
understand how we put our automation discipline to work and the pitfalls of
traditional small-step semantics in a mechanized development.

Let us recall the context of this proof. We have a relation ~ matching reduc-
tion states in continuation-based small-step semantics to terms of the traditional
small-step semantics. ~ informally reconstructs the term from a reduction state
by applying the continuation stack. Then, we have t → t' and continuation-
based semantics states s such that s ~ t. We are looking for s' such that s' ~ t'
and s ↛^+ s'. We do an induction on the stack size of the continuation of s, as
Lemma 1 helps us deal with the heredity proof of this induction and lets us
focus on the cases where the continuation κ in s is empty. Then, we perform an
induction on t → t'; in each induction case, we can get more information on s
because of the invariant s ~ t. This information allows us to case analyse on s
efficiently, and for each remaining case deduce s' by applying automatically ↛^>
reduction steps to s. We finally prove for each of those s', that s' ~ t'.

To illustrate the involved proof tactics, let us detail the step where we want
to translate the properties we know on t to s. For instance, if t is a value, we want
to derive that in s, the current expression is a value too and the continuation κ
only contains $k_{\text{ret}}$. This is done via a custom inversion tactic similar to the smart inversion described in Section 4.1. Additionally, we use reduction lemmas and simulation-helping lemmas to facilitate the proof. For instance, thanks to the information learned about $\kappa$ (it only contains $k_{\text{ret}}$), we later apply many steps at the same time, and show $\sim$ between the obtained state $s'$ and $t'$.

We have chosen to do our main induction on the size of continuation of $s$, whereas the natural strategy would have been to do it on $t \to t'$ itself. However, this leads to difficult times in Rocq because of the recursive nature of $t \to t'$ (see Section 3.1). Here, even though Rocq induction principle seems to work, doing the induction on the recursive $t \to t'$ creates induction hypotheses that are unusable, because variables and original hypotheses are not automatically correctly generalized (as they include equalities that prevent generalization and do not hold in our proof context).

To do an induction on $t \to t'$, one needs to carefully generalize the hypotheses in each case so as to create an induction hypothesis which is both usable (not contradictory) and precise enough to prove the final goal. This careful generalization is tedious to do, and breaks easily with updates to the proof, making proof repair difficult. Overall, by leveraging the regular nature of the continuation-based semantics judgments, our alternative proof strategy is more amenable to our proof automation discipline. Indeed, the continuation of a term contains the context in which the term occurs, and thus hides information that previously generated wrong hypotheses. So with continuations, we do not need to generalize anymore and reuse directly the induction principles generated by Rocq. In the end, we find it to be more maintainable and readable, again supporting our claim in favor of continuation-based semantics in mechanized developments. The term occurs, and thus hides information that previously generated wrong hypotheses.

# 5 Related Work

While this paper is, to our knowledge, the first to explain the advantages of using continuation-based small-step semantics to scale up mechanized proofs, a number of related works mention proof engineering difficulties associated to their semantics mechanization. Moreover, the use of continuation-based small-step semantics has already been pioneered in an array of relevant articles.

*Scaling-up mechanized developments about semantics* Scaling up mechanized developments from toy languages to real-life languages is challenging, and much work has been done in this area.

CakeML [17] is a verified compiler for a substantial subset of Standard ML, large enough to bootstrap itself. The semantics of the many intermediate languages of CakeML use a big-step style, specifically a variant called functional big-step semantics [25]. The use of big-step semantics avoids the bookkeeping of traditional small-step semantics and scales up better, but it cannot always be transferred to other languages where the order of evaluation matters, typically in presence of side-effects.
Another formally verified compiler for a functional language is CertiCoq, a
compiler for the specification language of Rocq. The intermediate languages of
CertiCoq use big-step semantics. Paraskevopoulou and Grover [26] define a new
simulation relation to prove the correctness of a continuation-passing style (CPS)
transformation (used in CertiCoq) and rely on logical relations to avoid ex-
plicit accounting for α-conversions, thereby simplifying their proofs. Their proof
technique holds for both big-step and small-step semantics of source languages,
whereas the target language is defined using step-indexed logical relations. Their
goal is to overcome the well-known complications of CPS correctness, particularly
related to α-conversion and administrative reductions. In contrast to their work,
we use De Bruijn indices and explicit environments, avoiding α-equivalence. To
end our tour of verified compilers, we can also consider Vélus [7], which proves
the correctness of a large subset of Lustre using CompCert. Vélus uses a mix
of inductive and co-inductive objects to express relations between streams of
values. Interestingly, their main correctness proofs follow the same outline we
described: induction on an object, inversion on other inductive hypotheses, and
reconstructing the proof in each case. Moreover, in their paper [7, Section 3.2],
they highlight the difficulty of discovering the details required to mechanize a
proof. These details are typically found while writing the proof and often require
modifications to the theorem's hypotheses and semantic definitions.

Outside of verified compilers, domain-specific mechanized developments using
language semantics also report difficulties for scaling up their proofs. Benzaken
et al. [2] prove the correctness of an SQL to IMP scheduler by defining their
semantics using big-step semantics. Similar to Vélus, their proof is not automated
and requires keeping the language small to remain tractable. For example, they
avoid using if-then-else in one of their intermediate languages, expressing it
through other constructs, though at the cost of increasing the length of the
generated code. Another key application of mechanized proof developments for
software verification concerns cryptography. The lines of work around Fiat [11,
12] or the recent Noise* [14] rely on synthesis and meta-programming inside the
proof assistant to generate verified code from a high-level specification. These
techniques, like other recent works [13], allow for a very high degree of proof
automation, at the expense of a large proof infrastructure that may be tedious
to maintain and expand. Instead, the kind of automation we promote is quite
basic and relies on cleverly using Rocq's primitive tactics and a lightweight,
adaptable proof strategy.

***Uses of continuation-based semantics*** Some other related work have already successfully used continuation-based small-step semantics in their formalization. First, Appel and Blazy [1] present a continuation-based small-step semantics for the Cminor language of CompCert. They define a sound separation logic with respect to a big-step operational semantics; their language is imperative, whereas ours is functional. While they focus on Cminor, they report that their continuation-based small-step semantics “allow a uniform representation of statement execution”, without expanding. We basically extend this claim and explain the inner workings of how it improves proof automation in proof assistants.
More recently, continuation-based small-step semantics were incorporated in the Skeletal semantics framework [5]. They aim to provide general tooling for defining and manipulating operational semantics and various interpretations. Skeletal semantics were used on toy languages to derive interpreters or static analyzers automatically from operational semantics. To improve automation in skeletal semantics, Khayam and Schmitt [16] define a purely functional meta-language that captures target language features and introduces continuations to derive continuation-based semantics. The handling of continuations in our rules is inspired by their meta-handling of continuations. Additionally, Courant et al. [9] use continuation-based semantics for the paper proof of the corectness of their code generator, and claim they could be “easily mechanized”.

Going beyond semantics, using syntactic artefacts like abstract machines to efficiently encode judgments in a proof assistant seems to have a broader application scope. Li and Appel [19] encode program transformations in a similar fashion, using MetaCoq [32] to enable proof sharing between different transformations. However, the correctness proof for their transformations still requires significant work: they focus more on extracting efficient implementations of transformations rather than easing their mechanized proof development.

# 6 Conclusion

The shape and details of semantic judgments inside the proof assistant directly influences the proof experience for all the theorems involving the semantics. Hence, it is worth the time to ponder and correctly choose how these judgments will be encoded before diving into the rest of the mechanized development. While traditional operational semantics use a recursive inductive judgment, handling it becomes tedious in a proof assistant. Specifically, automating proofs about traditional small-step semantics requires a significant effort in building ad-hoc proof automation frameworks, that themselves can become tricky to maintain.

Instead, we rely on a syntactic notion of continuations to represent recursivity in the judgments. This style based on continuations gives inductive judgments with no recursive premises, and a much more regular shape of inference rules. While harder to parse and compare to a pen-and-paper presentation, continuation-based small-step semantics play along very well with the basic tactics of proof assistants like Rocq, and allow for building cheap-yet-powerful automation that unlocks scaling up the development.

After having exposed the underlying reasons why continuation-based small-step semantics are easier to automate in a mechanized setting, and our case study on the Catala domain-specific language, we will try in future work to apply our proof automation methodology to bigger and more real-world projects to see how far this boost gets up.

# References

1. Appel, A.W., Blazy, S.: Separation Logic for Small-Step CMinor. In: Schneider, K., Brandt, J. (eds.) Theorem Proving in Higher Order Logics, 20th International
Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4732, pp. 5-21, Springer (2007), URL https://doi.org/10.1007/978-3-540-74591-4_3

2. Benzaken, V., Contejean, E., Hachmaoui, M.H., Keller, C., Mandel, L., Shinnar, A., Siméon, J.: Translating Canonical SQL to Imperative Code in Coq. Proc. ACM Program. Lang. 6 (OOPSLA1) (Apr 2022), https://doi.org/10.1145/3527327, URL https://doi.org/10.1145/3527327

3. Blazy, S.: From Mechanized Semantics to Verified Compilation: the Clight Semantics of CompCert. In: Beyer, D., Cavalcanti, A. (eds.) Fundamental Approaches to Software Engineering - 27th International Conference, FASE 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Lecture Notes in Computer Science, vol. 14573, pp. 1-21, Springer (2024), https://doi.org/10.1007/978-3-031-57259-3_1, URL https://doi.org/10.1007/978-3-031-57259-3_1

4. Blazy, S., Leroy, X.: Mechanized Semantics for the Clight Subset of the C Language. Journal of Automated Reasoning 43(3), 263-288 (2009), https://doi.org/10.1007/s10817-009-9148-3, URL https://hal.inria.fr/inria-00352524

5. Bodin, M., Gardner, P., Jensen, T.P., Schmitt, A.: Skeletal Semantics and their Interpretations. Proceedings of the ACM on Programming Languages 3, 1-31 (2018), URL https://api.semanticscholar.org/CorpusID:52846325

6. Bourke, T., Brun, L., Dagand, P., Leroy, X., Pouzet, M., Rieg, L.: A Formally Verified Compiler for Lustre. In: Cohen, A., Vechev, M.T. (eds.) Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017, pp. 586-601, ACM (2017), https://doi.org/10.1145/3062341.3062358, URL https://doi.org/10.1145/3062341.3062358

7. Bourke, T., Pesin, B., Pouzet, M.: Verified Compilation of Synchronous Dataflow with State Machines. ACM Transactions on Embedded Computing Systems 22(5s), 137:1-137:26 (Sep 2023), https://doi.org/10.1145/3608102, URL https://velus.inria.fr/emsoft2023/, eSWEEK special issue including presentations at the 23rd Int. Conf. on Embedded Software (EMSOFT 2023)

8. Correnson, A., Steinhöfel, D.: Engineering a Formally Verified Automated Bug Finder. In: Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, p. 1165-1176, ESEC/FSE 2023, Association for Computing Machinery, New York, NY, USA (2023), ISBN 9798400703270, https://doi.org/10.1145/3611643.3616290, URL https://doi.org/10.1145/3611643.3616290

9. Courant, N., Séré, A., Shankar, N.: The correctness of a code generator for a functional language. In: Verification, Model Checking, and Abstract Interpretation: 21st International Conference, VMCAI 2020, New Orleans, LA, USA, January 16-21, 2020, Proceedings 21, pp. 68-89, Springer (2020)

10. Delahaye, D.: A Tactic Language for the System Coq. In: Logic for Programming and Automated Reasoning: 7th International Conference, LPAR 2000 Reunion Island, France, November 6-10, 2000 Proceedings 7, pp. 85-95, Springer (2000)

11. Delaware, B., Pit-Claudel, C., Gross, J., Chlipala, A.: Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. Acm Sigplan Notices 50(1), 689-700 (2015)
12. Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Simple High-Level Code for Cryptographic Arithmetic: With Proofs, Without Compromises. ACM SIGOPS Operating Systems Review **54**(1), 23–30 (2020)

13. Grégoire, B., Léchenet, J.C., Tassi, E.: Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi. In: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 167–181, ACM, Boston MA USA (Jan 2023), ISBN 9798400700262, https://doi.org/10.1145/3573105.3575683, URL https://dl.acm.org/doi/10.1145/3573105.3575683

14. Ho, S., Protzenko, J., Bichhawat, A., Bhargavan, K.: Noise: A Library of Verified High-Performance Secure Channel Protocol Implementations. In: 2022 IEEE Symposium on Security and Privacy (SP), pp. 107–124, IEEE (2022)

15. Jourdan, J.H.: Verasco: a Formally Verified C Static Analyzer. Ph.D. thesis, Universite Paris Diderot-Paris VII (2016)

16. Khayam, A., Schmitt, A.: A Practical Approach for Describing Language Semantics. Submitted for publication (2022)

17. Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: A verified implementation of ML. In: Principles of Programming Languages (POPL), pp. 179–191, ACM Press (Jan 2014), https://doi.org/10.1145/2535838.2535841, URL https://cakeml.org/popl14.pdf

18. Lawsky, S.B.: A Logic for Statutes. Florida Tax Review (2018)

19. Li, J.M., Appel, A.W.: Deriving Efficient Program Transformations From Rewrite Rules. Proc. ACM Program. Lang. **5**(ICFP) (Aug 2021), https://doi.org/10.1145/3473579, URL https://doi.org/10.1145/3473579

20. Merigoux, D.: Proof-Oriented Domain-Specific Language Design for High-Assurance Software. Theses, Université Paris sciences et lettres (Dec 2021), URL https://tel.archives-ouvertes.fr/tel-03622012

21. Merigoux, D.: Experience Report: Implementing a Real-World, Medium-Sized Program Derived from a Legislative Specification. In: Programming Languages and the Law 2023 (affiliated with POPL), Boston (MA), United States (Jan 2023), URL https://inria.hal.science/hal-03933574

22. Merigoux, D., Chataing, N., Protzenko, J.: Catala: A programming language for the law. Proc. ACM Program. Lang. **5**(ICFP) (Aug 2021), https://doi.org/10.1145/3473582

23. Merigoux, D., Monat, R., Protzenko, J.: A modern compiler for the french tax code. In: Proceedings of the 30th ACM SIGPLAN International Conference on Compiler Construction, p. 71–82, CC 2021, Association for Computing Machinery, New York, NY, USA (2021), ISBN 9781450383257, https://doi.org/10.1145/3446804.3446850

24. Nipkow, T., Klein, G.: Concrete Semantics. with Isabelle/HOL **29** (2016)

25. Owens, S., Myreen, M.O., Kumar, R., Tan, Y.K.: Functional Big-Step Semantics. In: European Symposium on Programming (2016), URL https://api.semanticscholar.org/CorpusID:4864472

26. Paraskevopoulou, Z., Grover, A.: Compiling with Continuations, Correctly. Proc. ACM Program. Lang. **5**(OOPSLA) (oct 2021), https://doi.org/10.1145/3485491, URL https://doi.org/10.1145/3485491

27. Pédrot, P.M.: Ltac2: Tactical Warfare. In: The Fifth International Workshop on Coq for Programming Languages, CoqPL, vol. 2019 (2019)

28. Pierce, B.C., Casinghino, C., Gaboardi, M., Greenberg, M., Hriţcu, C., Sjöberg, V., Yorgey, B.: Software Foundations (2010), URL Webpage: http://www.cis.upenn.edu/bcpierce/sf/current/index.html
29. Pit-Claudel, C.: Compilation Using Correct-by-Construction Program Synthesis. Master's thesis, Massachusetts Institute of Technology (August 2016), https://doi.org/1721.1/107293, URL http://pit-claudel.fr/clement/MSc/

30. Ringer, T.: Proof Repair. Ph.D. thesis, University of Washington (2021)

31. Ringer, T., Sanchez-Stern, A., Grossman, D., Lerner, S.: REPLica: REPL Instrumentation for Coq Analysis. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 99–113, CPP 2020, Association for Computing Machinery, New York, NY, USA (2020), ISBN 9781450370974, https://doi.org/10.1145/3372885.3373823, URL https://doi.org/10.1145/3372885.3373823

32. Sozeau, M., Anand, A., Boulier, S., Cohen, C., Forster, Y., Kunze, F., Malecha, G., Tabareau, N., Winterhalter, T.: The MetaCoq Project. Journal of Automated Reasoning **64**(5), 947–999 (Jun 2020), ISSN 1573-0670, https://doi.org/10.1007/s10817-019-09540-0, URL https://doi.org/10.1007/s10817-019-09540-0