<figure><img src="image_46.png" /><figcaption>Figure 4: Structure of judgments for the source system</figcaption></figure>

(resp. module $X = P$) and deleting constraints $S$ with type $t := \tau$ (resp. module $X := P$). We believe that they do not impact the overall structure of the system, only adding more cases in the set of rules. We did not include first-class modules.

## 2.2 System structure and judgments

The typing judgment uses several auxiliary judgments whose dependencies are presented in Figure 4. The system we present revolves around two main components: *typing* (for module expressions and signatures) and *subtyping*. The *path-based* representation of type sharing in OCAML modules requires us to define two more judgments: *equivalence* and *strengthening*. Finally, as retrieving signatures in the environment is non trivial, we define a pair of *resolution* helper judgments. We present and explain these judgments in reversed order of dependency in the subsequent subsections.

## 2.3 Resolution

In the OCAML module system, retrieving the signature of a given path (of a module stored in the environment) is not as simple as a lookup. First, objects are stored with multiple levels of indirection (like $X.X' \cdot X''$) which requires to inspect intermediary signatures. Secondly, every signature can be a module type variables, which must also be resolved to its definition before accessing a field. For this purpose, we recursively define a *path resolution* judgment $\Gamma \vdash P \triangleright S$ which gives the signature $S$ of a path $P$ and a *signature resolution* judgment $\Gamma \vdash Q.T \Leftrightarrow S$, which retrieves the definition $S$ of a module type $Q.T$ (both in an environment $\Gamma$).

We show below two examples of resolution rules. Rule S-RES-MODTYPE links path resolution and signature resolution: if the path resolution of $P$ returns a module type $Q.T$, the definition of $Q.T$ should be resolved to a signature $S$. Rule S-RES-PROJ-MOD accesses a submodule $X$ of a module path $P$. This rule illustrates the transformation of *local* links in the signature $S$ (that might refer to other components of the module at $P$ via its self-reference $A$) into *absolute* ones by substitution of the self-reference $A$ for the path $P$. The full set of rules is given in §C.1.

$$ \frac{\substack{\text{S-RES-MODTYPE} \\ \Gamma \vdash P \triangleright Q.T}}{\substack{\text{S-RES-PROJ-MOD} \\ \Gamma \vdash P \triangleright S}} \qquad \frac{\substack{\text{S-RES-MODTYPE} \\ \Gamma \vdash P \triangleright \text{sig}_A \bar{D} \text{end}}}{\substack{\text{S-RES-PROJ-MOD} \\ \Gamma \vdash P.X \triangleright S[A \mapsto P]}} $$

$$ \frac{\text{S-RES-MODTYPE}}{\text{S-RES-PROJ-MOD}} \qquad \frac{\text{S-RES-MODTYPE} \quad \text{S-RES-PROJ-MOD}}{\text{S-RES-PROJ-MOD}} \qquad (\text{module } X : S) \in \bar{D} $$

## 2.4 Equivalence

In the path-based approach of OCaml, several paths can resolve to the same type, as illustrated in §1.1. A type definition can have several *equivalent* expressions, called aliases. This leads us to consider a notion of *type equivalence* based on the existence of a common ancestor when browsing the type sharing tree of aliases. This can be seen in the rules S-EQV-TYPE-RES and
<figure><img src="image_47.png" /><figcaption>Example 2: Two equivalent signatures $S_1$ and $S_2$: they define two different type sharing trees that yet have the same connected components. Specifically, two types are aliases in $S_1$ if and only if they are also aliases in $S_2$.</figcaption></figure>

<figure><img src="image_48.png" /><figcaption>Example 3: Strengthening and its graphical interpretation</figcaption></figure>

**S-EQV-TYPE-LOCAL:** a type is equivalent to its definition (and only to itself for abstract types). With transitivity, symmetry, and reflexivity, we get an equivalence relationship on types.

$$ \frac{\Gamma \vdash_{\text{src}} P \triangleright \text{sig}_A \bar{D} \text{ end} \quad (\text{type}t = \tau) \in \bar{D}}{\Gamma \vdash_{\text{src}} P.t \approx \tau[A \mapsto P]} $$

$$ \frac{\Gamma \vdash_{\text{src}} (A.t : \text{type}t = \tau) \in \Gamma}{\Gamma \vdash_{\text{src}} A.t \approx \tau} $$

Building on this type equivalence, we define *signature equivalence*: two signatures are equivalent if we can go from the first one to the second one by only substituting type aliases. This is illustrated by the two signatures in Example 2. The full set of rules is given in §C.2.

## 2.5 Strengthening

The need for strengthening is illustrated in Example 3. When aliasing the module `M` on line 7, the inferred signature for `N` cannot be straightforwardly obtained by copying the signature of `M` without loss of type-sharing. Indeed, `M` defines an abstract type which is a root of a connected component of the underlying type-sharing tree. Duplicating the signature duplicates the root, effectively creating a separated connected component and thus, a new abstract type. The known solution to this problem is to use a *strengthening* operation $\Gamma \vdash P/S \gg S'$ of a signature `S` by a path `P`, producing `S'`, a *strengthened* version of `S` where each abstract type field has been rewritten into a concrete type field pointing to its original definition in `P`.

Rule S-STR-SIG-SIG shows the case for declarations inside a signature. Our technical choice of having abstract types represented as pointers to themselves ($\text{type}t = A.t$) makes the definition of strengthening easy, as substituting the self-reference for the path suffices to transform local links into absolute ones ($\text{type}t = P.t$). Thus, strengthening does not change declarations, except
for submodules (rule `S-STR-DECL-MOD`) where the signature is strengthened with the extended path `P.X`.Functor signatures are not strengthened, as they do not introduce new abstract types. The full set of rules is given in §C.3.

$$ \frac{\Gamma \vdash \overline{D}[A \mapsto P]/P \gg \overline{D}'}{\Gamma \vdash \operatorname{sig}_A \overline{D} \text{ end}/P \gg \operatorname{sig}_A \overline{D}' \text{ end}} $$

$$ \frac{\Gamma \vdash S / (P.X) \gg S'}{\Gamma \vdash (\text{module } X : S) / P \gg \text{module } X : S'} $$

## 2.6 Subtyping

The subtyping judgment has a fundamental role in the OCAML module system, as it allows the user to define an abstract (polymorphic) interface and assign it to a module that has a richer signature than this interface. In OCaml, some (but not all) subtyping operations have computational content: the removal and reordering of fields implies a runtime copy of the memory representation of the module. We thus distinguish two operations: *Subtyping by abstraction*, written $\Gamma \vdash^{\text{src}} S_1 \triangleleft: S_2$, which has no computational content and *Subtyping*, written $\Gamma \vdash^{\text{src}} S_1 <: S_2$, which includes the former and also allows for removal and reordering of fields and therefore has some computational content. Both judgments have the same rules, except for the comparison of structural signatures.

Subtyping on signatures enforces a structural match (up to name resolution): functor signature against functor signature and structural signature against structural signature. The latter case is where the only distinction between the two modes of subtyping appears: in subtyping by abstraction, the two lists of declarations $\overline{D}$ and $\overline{D}'$ are compared directly as shown in rule `S-SUB-SIG-SIG`. In the general form of subtyping, a subset $\overline{D}_0$ of the declaration list $\overline{D}$ is compared with $\overline{D}'$, allowing for reordering and deletion, as shown in Rule `S-SUB-SIG`. Using a subset instead of a subsequence allows for reordering.

$$ \frac{\Gamma, \overline{A.D} \vdash^{\text{src}} \overline{D} \triangleleft: \overline{D}'}{\Gamma \vdash^{\text{src}} \operatorname{sig}_A \overline{D} \text{ end} \triangleleft: \operatorname{sig}_A \overline{D}' \text{ end}} $$

$$ \frac{\overline{D}_0 \subseteq \overline{D} \qquad \Gamma, \overline{A.D} \vdash_A^{\text{src}} \overline{D}_0 <: \overline{D}'}{\Gamma \vdash^{\text{src}} \operatorname{sig}_A \overline{D} \text{ end} <: \operatorname{sig}_A \overline{D}' \text{ end}} $$

In both rules, the subtyping is done *declaration by declaration* (independently), in an environment that contains all the declarations of the richer (left-hand-side) signature. This approach matches well with our representation choice of abstract types, allowing us to have only one rule for comparing both abstract types and concrete types declarations (rule `S-SUB-DECL-TYPE`). The other subtyping rules for declarations are straightforward, and depends on signature subtyping. As a module type field can be used in both covariant and contravariant positions (as functor arguments for example), the rule for subtyping a module type declaration checks subtyping in both directions. In §C.4 and in the following, the rules that are similar between abstraction and general subtyping are given with the symbol `<`: being either `<`: or `<>`:

$$ \frac{\Gamma \vdash^{\text{src}} \tau <: \tau'}{\Gamma \vdash_A^{\text{src}} (\text{type } t = \tau) <: (\text{type } t = \tau')} $$

$$ \frac{\Gamma \vdash^{\text{src}} S <: S'}{\Gamma \vdash_A^{\text{src}} (\text{module type } T = S) <: (\text{module type } T = S')} $$

## 2.7 Typing

Once all the auxiliary judgments have been laid out, the typing judgment is mostly straightforward. All rules are given in §C.5. The judgments for signature typing $\Gamma \vdash^{\text{src}} S : \checkmark$ and declarations
typing $\Gamma \vdash_A^{\text{src}} D : \check{\text{✓}}$ ensure that no shadowing occurs and no free variables are used. We omit the rules here. The judgment for bindings $\Gamma \vdash_B^{\text{src}} D$ uses a core-language typing judgment for expressions and typing of signatures, and is mutually recursive with the typing of modules (for submodules). The rules are straightforward and omitted.

**Module typing** The judgment for modules contains both syntax-directed and free-floating rules, making the presentation purposefully logical rather than algorithmic. There is an equivalent algorithmic presentation, but it is more involved and hides the key insights of the separation of operations between resolution, equivalence, strengthening, subtyping, and typing. Besides, the equivalent, canonical model that we propose in the next section is better suited for deriving algorithmic presentations for the source system. Free-floating typing rules must have no computational content. Therefore, general subtyping (which has some computation content), is not free floating: it should only be used at specific program points, namely functor application and signature ascription, where the target signature of the runtime coercion is explicit in the source. While having no computational content, subtyping by abstraction is still not made free-floating to prevent unnecessary abstraction of types (which would lead to loss of type-sharing). The syntax-directed rules are as follows:

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

Functor application (Rule S-TYP-MOD-APP) is normally a place where *signature-avoidance* may occur. In our presentation however, the restriction of functor application to paths prevents this issue. Indeed, as all the abstract types of the argument are defined in the context, no type field is hidden by the application, and thus, no escaping of scope can occur. In contrast, as the grammar allows projection on any module expression (which can hide type fields and could trigger signature avoidance), the projection rule S-TYP-MOD-PROJ is designed to tackle the issue. The abstraction subtyping $\Gamma, \bar{D}_1 \vdash_S^{\text{src}} S \triangleleft S'$ allows for cutting the links to types in $S$ that will become inaccessible *outside* of the signature of $M$, i.e., without the fields declared in $\bar{D}_1$, so that the resulting signature $S'$ is wellformed in $\Gamma$. This rule is however too permissive, as we allow to *implicitly* abstract *more than necessary* and lose some type sharing. Additional conditions to prevent *unnecessary* loss of type sharing could be added to this rule, but they would be complex to write down in this setting. Fortunately, they will be easy to express using the canonical system.

**Free-Floating rules** Before doing a projection $M.X$, we must allow to *rewire* the type sharing tree so that types used in $X$ point to other aliases (either external ones, i.e., accessible outside
of M, or local ones, accessible inside of X). Similarly, we must allow strengthening to keep sharing information between aliases. This leads to two additional free-floating rules:

$$ \frac{\Gamma \vdash_P S \qquad \Gamma \vdash S/P \gg S'}{\Gamma \vdash_P S'} $$

$$ \frac{\Gamma \vdash M : S \qquad \Gamma \vdash S \approx S'}{\Gamma \vdash M : S'} $$

**Remarks on the source system** While this declarative presentation of the source system may appear relatively simple, it actually suffers from three main issues. First, it relies on the equivalence judgment to guess correct rewritings in signatures. Second, type sharing can be lost when projecting on a submodule via over-abstraction. Thirdly, the strengthening judgment may seem ad-hoc, while being necessary to prevent loss of type-sharing. In current OCaml, these problems are partially solved via heuristics which are sufficient in simple cases, but fail for more advanced uses of modules. We now study a canonical presentation of the module system that solves all three issues.

# 3 Canonical signatures and existential types

Some issues of the source presentation come from the ambiguity and weaknesses of the path-based type-sharing. In this section, we present an alternative set of typing rules with an extended syntax for signatures inspired by previous work on representation of modules in $F^\omega$. This system, called *canonical*, has simpler typing judgments and does not suffer from the signature avoidance problem. We show that the canonical system is more expressive than the source one, as every module expression that can be typed in the source system can also be typed in the canonical system with a signature that has at least the same amount of type sharing.

## 3.1 The need for existential types

In the source presentation, maintaining the connected components of the type sharing tree throughout projection —where fields can be deleted— sometimes require rewriting type equalities (through equivalence) or abstracting type fields (through abstraction subtyping). The core issue is that source signatures store type equalities via a type sharing tree that is cumbersome to handle. However, the information we are actually interested in is not the type sharing tree itself, only the connected components. To handle those directly, we introduce an *existential type* that acts as a canonical representative of the equivalence class. In the type sharing tree, it can be seen as an additional point with a special status, and the whole tree is flattened to one level of depth, as illustrated in Example 4. Rooted with an existential type that cannot be deleted, the connected components become insensible to the loss of some type fields. Building on this intuition, we present a new system, called *canonical*, where signatures use quantifiers to handle abstract types.

## 3.2 System structure and judgments

The grammar of the language, given in Figure 5, extends the OCAML grammar of Figure 3. Crucially, the source syntax (for modules and signatures) remains the same, including source signatures, while new syntactical categories are introduced to represent canonical signatures (and canonical types). By convention, we use curvy capitals ($R, S, D, ...$) for canonical objects.
<figure><img src="image_50.png" /></figure>

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

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

<figure><img src="image_53.png" /><figcaption>Example 4: Comparison between the source and canonical signatures and their associated type-sharing trees. Canonical signatures are extended with an existential binder that acts as a special anchor point for the tree.</figcaption></figure>

<figure><img src="image_54.png" /><figcaption>Figure 5: Syntax extensions of the *canonical* module language.</figcaption></figure>

We distinguish between *manifest* canonical signatures $\mathcal{R}$ that only refer to abstract types bound in the context and *abstract* canonical signatures $\exists\bar{\alpha}.\mathcal{R}$ (written $\mathcal{S}$) that also specify the existential types $\bar{\alpha}$ created by the module. Notice that canonical manifest signatures cannot refer to other signatures (e.g., using paths), as these are always inlined. Signatures of functors are polymorphic in the abstract types provided by the argument: indeed, these should be treated abstractly, while they can also be returned and thus shared in the result. Signatures stored in module type declarations are just parameterized by their abstract types: these will later be existentially or universally quantified, depending on context. We use an $\mathcal{F}^\omega$ style $\lambda$-binding for these. As we will see in the typing rules, the grammar restricts the positions where abstract types are bounded (existentially or universally). For instance, inside a structural signature, all submodules have manifest signatures, while functor bodies may bound new abstract types.

Canonical signatures remove the need for resolution, equivalence, and strengthening, which significantly simplifies the overall presentation. The judgments are thus reduced to typing of modules (and bindings), typing of source signatures, which we enrich to produce a canonical signature, and subtyping.

## 3.3 Signature typing

We start with signature typing $\Gamma \vdash_S \lambda\bar{\alpha}.\mathcal{R}$ and declaration typing $\Gamma \vdash_A D : \lambda\bar{\alpha}.\mathcal{D}$, as they illustrate the key mechanism of *abstract type lifting*. The positions where abstract types are
bound are crucial to ensure the correct sharing of types. First, abstract types are introduced only by an abstract type declaration (Rule C-TYP-DECL-TYPEABS). Then, they are gathered and lifted from abstract type definitions and submodules to their parent module to ensure sharing between declarations in the same structure (rules C-TYP-DECL-MOD and C-TYP-DECL-SEQ). The lifting does not go through a functor definition (Rule C-TYP-SIG-FUNCTOR): indeed, in the generative case, each application of the functor should create new unrelated abstract types. The full set of rules are in §D.2.

$$ \frac{\text{C-TYP-DECL-TYPEABS}}{\Gamma \vdash_A \text{type } t = A.t : \lambda\alpha. \text{type } t = \alpha} $$

$$ \frac{\text{C-TYP-DECL-SEQ}}{\Gamma \vdash_A (D_1, \bar{D}) : \lambda\bar{\alpha}_1 \bar{\alpha}. (D_1, \bar{D})} $$

$$ \frac{\text{C-TYP-DECL-MOD}}{\Gamma \vdash_S : \lambda\bar{\alpha}.\mathcal{R}} \qquad A.X \notin \Gamma $$

$$ \frac{\text{C-TYP-SIG-FUNCTOR}}{\Gamma \vdash S_a : \lambda\bar{\alpha}.\mathcal{R}_a \qquad \Gamma, \bar{\alpha}, Y : \mathcal{R}_a \vdash S : \lambda\beta.R \qquad Y \notin \Gamma} $$

## 3.4 Subtyping

The subtyping between two canonical signatures $\exists\bar{\alpha}.\mathcal{R}$ and $\exists\bar{\alpha}'.\mathcal{R}'$ is similar to the source subtyping, with the addition of the mechanism to deal with quantifiers.

Rule C-SUB-SIG-MATCH allows us to compare abstract signatures, while the other subtyping rules deal with concrete signatures. The types $\bar{\alpha}$ created by the left-hand-side signature are made available (i.e., pushed in the context), while the right-hand-side ones $\bar{\alpha}'$ are instantiated with some types $\bar{\tau}$. If both signatures define the same abstract types (up to $\alpha$-conversion), a simple renaming instantiation $\bar{\alpha} \mapsto \bar{\alpha}'$ is sufficient. Otherwise, the left-hand-side signature $\mathcal{R}$ can be less abstract (i.e., binding fewer abstract types) than the right-hand-side one $\mathcal{R}'$, in which case some right-hand side abstract types are instantiated with concrete types.

For functor signatures (Rule C-SUB-SIG-FUNCTOR), the parameter is in a contravariant position, hence we check subtyping of the argument signatures in reverse order. As with the source presentation, we distinguish between two kinds of subtyping: abstraction-only subtyping $\Gamma \vdash_S S_1 \prec: S_2$ and general subtyping $\Gamma \vdash S_1 \prec: S_2$, which allows both abstraction and deletion of fields. They differ only by the rules C-SUB-SIG-SIG vs. C-SUBEQ-SIG-SIG. In §D.1 and in the following, the rules that are similar between abstraction and general subtyping are given with the symbol $\prec$: being either $\prec$: or $\prec$:

$$ \frac{\text{C-SUB-SIG-MATCH}}{\Gamma, \bar{\alpha} \vdash_R \mathcal{R} \prec: \mathcal{R}'[\bar{\alpha}' \mapsto \bar{\tau}]} $$

$$ \frac{\text{C-SUB-SIG-FUNCTOR}}{\Gamma, \bar{\alpha}' \vdash_R \mathcal{R}' \prec: \mathcal{R}[\bar{\alpha} \mapsto \bar{\tau}]} \qquad \Gamma, \bar{\alpha}', (Y : \mathcal{R}') \vdash_S S[\bar{\alpha} \mapsto \bar{\tau}] \prec: S' \qquad Y \notin \Gamma $$

$$ \frac{\text{C-SUB-SIG-SIG}}{\Gamma \vdash \text{sig}_A \bar{D} \text{ end} \prec: \text{sig}_A \bar{D}' \text{ end}} $$

$$ \frac{\text{C-SUBEQ-SIG-SIG}}{\Gamma \vdash \bar{D} \prec: \bar{D}'} $$

## 3.5 Typing

As with subtyping, the use of canonical signatures and existential types makes the typing simpler and syntax directed. The key technical point is the lifting of the existential quantification that
happens during typing, as already explained for the signature typing in §3.3.

**Bindings typing** The rules presented below for typing a binder give a list of canonical declarations *alongside* a list of (created) existential types. The signature typing judgment is used to convert source types and signatures (as in Rule C-TYP-DECL-MODTYPE for instance) into canonical types and signatures.

$$ \begin{array}{c} \text{C-TYP-DECL-MOD} \\ \Gamma \vdash_A M : \exists \bar{\alpha}. \bar{R} \\ \Gamma \vdash_A (\text{module } X = M) : \exists \bar{\alpha}. (\text{module } X : \bar{R}) \end{array} $$

$$ \begin{array}{c} \text{C-TYP-DECL-MODTYPE} \\ \Gamma \vdash_S : \lambda \bar{\alpha}. \bar{R} \\ \Gamma \vdash_A (\text{module type } T = S) : (\text{module type } T = \lambda \bar{\alpha}. \bar{R}) \end{array} $$

$$ \begin{array}{c} \text{C-TYP-DECL-SEQ} \\ \Gamma \vdash_A B_1 : \exists \bar{\alpha}_1. \bar{D}_1 \\ \Gamma \vdash_A B_1, \bar{B} : \exists \bar{\alpha}_1 \bar{\alpha}. \bar{D}_1, \bar{D} \end{array} $$

The existential types—which are lifted from submodules with Rule C-TYP-DECL-MOD—are merged by Rule C-TYP-DECL-SEQ, to extend their scope to the local enclosing module. For example, if a module *M* has a submodule *X* which defines an abstract type *α*, the existential quantification is lifted from the submodule *X* to the whole module *M*.

**Module expressions typing** Existential types are introduced only by explicit sealing (Rule C-TYP-MOD-SEALING). Applying a functor to its argument (Rule C-TYP-MOD-APP) can share the types of the argument via the substitution $[\bar{\alpha} \mapsto \bar{\tau}]$.

$$ \begin{array}{c} \text{C-TYP-STRUCT} \\ \Gamma \vdash_A B : \exists \bar{\alpha}. \bar{D} \\ \Gamma \vdash \text{struct}_A B \text{ end} : \exists \bar{\alpha}. \text{sig}_A \bar{D} \text{ end} \end{array} $$

$$ \begin{array}{c} \text{C-TYP-MOD-SEALING} \\ \Gamma \vdash_S : \lambda \bar{\alpha}. \bar{R} \\ \Gamma \vdash_P : \bar{R}' \\ \Gamma \vdash_{R'} : \mathcal{R} \prec : \mathcal{R}[\bar{\alpha} \mapsto \bar{\tau}] \\ \Gamma \vdash (P : S) : \exists \bar{\alpha}. \bar{R} \end{array} $$

$$ \begin{array}{c} \text{C-TYP-MOD-FUNCTOR} \\ \Gamma \vdash_S : \lambda \bar{\alpha}. \bar{R} \\ \Gamma, \bar{\alpha}, (Y : \bar{R}) \vdash_M : S \\ \Gamma \vdash (Y : S) \to M : \forall \bar{\alpha}. (Y : \bar{R}) \to S \end{array} $$

$$ \begin{array}{c} \text{C-TYP-MOD-APP} \\ \Gamma \vdash P : \forall \bar{\alpha}. (Y : \bar{R}) \to S \\ \Gamma \vdash P' : \bar{R}' \\ \Gamma \vdash_{R'} : \mathcal{R}' \prec : \mathcal{R}[\bar{\alpha} \mapsto \bar{\tau}] \\ \Gamma \vdash P(P') : S[\bar{\alpha} \mapsto \bar{\tau}] \end{array} $$

$$ \begin{array}{c} \text{C-TYP-MOD-PROJ} \\ \Gamma \vdash_M : \exists \bar{\alpha}. \text{sig}_A \bar{D}_1, \text{module } X : \bar{R}, \bar{D}_2 \text{ end} \\ \Gamma \vdash M.X : \exists \bar{\alpha}. \bar{R} \end{array} $$

In the source presentation, the projection rule S-TYP-MOD-PROJ is the only place where signature avoidance can arise, by cutting local links in unsolvable ways. We needed to allow for abstraction subtyping. In the canonical presentation (Rule C-TYP-MOD-PROJ), all the local links go through existentially quantified abstract types in front of the signature. By keeping all the existentially quantified types, projecting a component cannot cause signature avoidance: all the abstract types (that could go out of scope and cause signature avoidance issues) that *M.X* could use are in the list $\bar{\alpha}$ and remain bound in the signature of *M.X*. The full set of typing rules is given in §D.2.
## 3.6 From the source to the canonical system

Both presentations share the same grammar for module expressions and signatures, and thus have the same input for typing. By extending the typing predicate to environments (to check wellformedness), we can translate source judgments (resolution, equivalence, strengthening) into the canonical presentation. This translation—called canonification—gives insight on how the source mechanisms can be understood in the canonical framework.

**Typing of source environments** We translate environments with source signatures into their canonical counterparts, using signature typing, declaration typing, and the following rules:

$$ \begin{array}{c} \text{C-CF-EMPTY} \\ \vdash \emptyset \quad \vdash \emptyset \end{array} \qquad \begin{array}{c} \text{C-CF-FCTARG} \\ \Gamma \vdash \Gamma_s \qquad \Gamma \vdash S : \lambda \bar{\alpha}.R \\ \Gamma, \bar{\alpha}, (Y : R) \vdash \Gamma_s, (Y : S) \end{array} \qquad \begin{array}{c} \text{C-CF-DECL} \\ \Gamma \vdash \Gamma_s \qquad \Gamma \vdash_A D : \lambda \bar{\alpha}.D \\ \Gamma, \bar{\alpha}, (A.I : D) \vdash \Gamma_s, (A.I : D) \end{array} $$

**Canonification of resolution** We now state how the resolution behaves regarding canonification. The main difference between the two systems comes from the fact that abstract types are quantified outside of the signature in the canonical system (the signature is always concrete), while they are introduced anywhere inside source signatures (which may contain abstract type definitions). Thus, the source signature obtained via resolution of P and the canonical signature of P only differ by the presence of quantifiers.

$$ \Gamma_s \upharpoonright_{\text{src}} P \triangleright S \wedge \Gamma \upharpoonright_{\text{can}} \Gamma_s \wedge \Gamma \upharpoonright_{\text{can}} S : \lambda \bar{\alpha}.R \Rightarrow \Gamma \upharpoonright_{\text{can}} P : R \quad (1) $$

$$ \Gamma_s \upharpoonright_{\text{src}} Q.T \Leftrightarrow S \wedge \Gamma \upharpoonright_{\text{can}} \Gamma_s \wedge \Gamma \upharpoonright_{\text{can}} S : \lambda \bar{\alpha}.R \Rightarrow \Gamma \upharpoonright_{\text{can}} Q.T : \lambda \bar{\alpha}.R \quad (2) $$

**Canonification of strengthening** Via resolution, the introduction of abstract types is re-exposed by the signature. To prevent an actual duplication of abstract types, the source presentation relies on strengthening. While the resolution of a path P corresponds to a canonical signature with existential types bound in front, a strengthened signature can be made fully concrete (no quantified types): all types refer to their original definition through the path P. In the canonical presentation, this is a *no-op*, as all type definitions already go through the proper quantified existential types in the context:

$$ \Gamma_s \upharpoonright_{\text{src}} P \triangleright S \wedge \Gamma_s \vdash S/P \gg S' \wedge \Gamma \upharpoonright_{\text{can}} \Gamma_s \wedge \Gamma \upharpoonright_{\text{can}} S : \lambda \bar{\alpha}.R \Rightarrow \Gamma \upharpoonright_{\text{can}} S' : R \quad (3) $$

**Canonification of equivalence** As we described in the previous section, two equivalent signatures have the same connected components of their type sharing tree. In the canonical model, all connected components are flattened into a tree of depth 1, with an existentially quantified variable at the root. This means that two equivalent signatures actually have the same canonification, which matches the intuition (and naming) that canonical signatures are indeed *canonical*. We get the following result:

$$ \Gamma_s \upharpoonright_{\text{src}} S_1 \approx S_2 \wedge \Gamma \upharpoonright_{\text{can}} \Gamma_s \wedge \Gamma \upharpoonright_{\text{can}} S_1 : S_1 \wedge \Gamma \upharpoonright_{\text{can}} S_2 : S_2 \Rightarrow S_1 = S_2 \quad (4) $$

**Canonification of subtyping** As the rules of subtyping in the source and canonical systems are very similar, the two judgments are also very similar. The only difference is that source subtyping can lose type equalities by over-abstraction. However, in the canonical system, with
Rule C-SUB-SIG-MATCH, the correspondence between the abstract types is dealt with at the signature level, with no abstraction done at the declaration level. We get the following result:

$$ \Gamma_s \vdash_{\text{src}} S_1 <: S_2 \wedge \Gamma \vdash_{\text{can}} \Gamma_s \wedge \Gamma \vdash_{\text{can}} S_1 : S_1 \wedge \Gamma \vdash_{\text{can}} S_2 : S_2 \implies \Gamma \vdash_{\text{can}} S_1 <: S_2 \quad (5) $$

**Canonification of typing** Once all canonification results have been laid out, the typing result becomes easy to write. All typing derivations can be translated into canonical ones, with the only difference being that some over-abstraction during projections and resolutions can lead to a source signature having lost some type sharing. This type-sharing loss, can be delayed to the last step of the derivation (combining the losses of all the intermediary signatures), which gives the following result:

**Theorem 1 (Canonification of typing).** Considering any module expression *M* that admits a signature *S* in the source presentation, it also admits a corresponding canonical signature *S* with more type equalities:

$$ \Gamma_s \vdash_{\text{src}} M : S \wedge \Gamma \vdash_{\text{can}} \Gamma_s \wedge \Gamma \vdash_{\text{can}} S : S \implies \Gamma \vdash_{\text{can}} M : S' \wedge \Gamma \vdash_{\text{can}} S' <: S $$

This link between the source and canonical system shows the expressiveness of the latter one, but is only half of the story. Exploring at which conditions the canonical derivations can be translated back into the source will uncover a new concept: anchorability.

# 4 Anchoring: back to the source system

In this section we study the process of translating typing derivations from the canonical system back into the source system, which we call *anchoring*. As the canonical system is more expressive than the source one, it is not always possible to translate signatures back into the source syntax. Still, we can precisely exhibit the conditions under which anchoring is possible. This gives a new specification of the source system, which could also be used to improve the way signature avoidance is actually resolved in OCAML.

The canonical system thus provides the intuition, formal guarantees, and algorithmic insights for the design of OCAML's modules mechanisms.

## 4.1 Quantification vs structural information

The key insight is the semantic difference in the source syntax between the declaration of a concrete type (*type* *t* = *τ*) and that of an abstract type (*type* *t*). An abstract type declaration states the *introduction* of both a *new type* and of a *new field* that may later be used as a handle to refer to this abstract type, directly or indirectly via a path. For a signature used in a covariant position, an abstract type declaration effectively *creates* a new type (existential quantification) and *adds* a type field (structural information) to the signature. By contrast, a concrete type definition only introduces structural information—adding a field to refer to an existing type but without introducing a new type.

Canonical signatures *separate* the quantification information (existential, universal, or lambda binders) from the structural information (fields). Thus, it makes the scope of abstract types explicit, using the logical notion of binder, which is perfectly suited for that purpose. More importantly, it allows to refer to types that do not yet have a handle, while the source system cannot. This is illustrated in the following code:
1 | module X = (struct
2 |     module X0 = (... : sig type t end)
3 |     module X1 = struct
4 |         type u = X0.t * int
5 |         type v = X0.t * bool
6 |     end
7 | end).X1

10 | (* Canonical signature of X *)
11 | module X : ∃α. sig
12 |     type u = α * int
13 |     type v = α * string
14 | end

Here, a type definition (t) is lost when projecting only on the submodule X1. The source syntax *cannot* express the existence of a type that is the first component of both u and v without already having a handle to that type<fnref n="1" />: being forced to merge quantification and structural information limits the expressiveness. However, the module X can be given a canonical signature, where the two kinds of information are clearly separated.

This allows us to better describe the solvable and unsolvable cases of signature avoidance for the source presentation. In the *solvable* cases of signature avoidance, each use of an abstract type has an *in-scope* alias (that can serve as a handle) defined before the type is used. In such cases, the quantification and structural information coincide in a way expressible by the source syntax. In other cases, signature avoidance is *unsolvable*.

## 4.2 Anchoring of canonical signatures

Building on the insights of the previous subsection, we can describe the *anchoring* process that translates a canonical signature back into the source system when the quantification and structural information coincide. The main mechanism boils down to identifying the first place where an abstract type $\alpha$ is used. If it is at the top level of a type declaration $type t = \alpha$, we say that the existential type $\alpha$ is *anchorable*. In the corresponding source signature, we can make *t* an abstract type definition, creating a handle to *t* that can then be used instead of $\alpha$ in the canonical signature. The type *t* must be the *first* reference to the abstract type $\alpha$, regardless of whether or not it is the original definition point. If the type $\alpha$ is used earlier, we raise a signature avoidance failure.

**Example 5** illustrates the process of finding the first available position to rewire the type-sharing tree of **Example 1**. We see the change of the defining instance of $\alpha$, from $X.t$ to $Y.a$ after a projection that makes $X.t$ and $X.u$ unreachable.

The anchoring process consists of associating abstract types with their first available aliases, which we gather using an *anchoring map* $\theta : \alpha \mapsto Q.t$. We define a signature anchoring judgment $\Gamma \vdash_S \alpha \leftrightarrow \Gamma_s; \theta_{\Gamma} \vdash_S \alpha$ that, given an environment $\Gamma$ and a canonical signature $S$, produces a source environment $\Gamma_s$ associated with an anchoring map $\theta_{\Gamma}$ and a source signature $S$ associated with an anchoring map $\theta$. In a nutshell, the judgment produces the source counterpart of the canonical signature $S$ by gathering the handles of the abstract types, and replacing the uses of abstract types by their handles. The full set of rules is given in §D.3.

Using the anchoring judgment, we define *anchorable typing*, written $\Gamma \vdash^{anc} M : S$. The judgment is defined by a copy of the typing rules for the judgment $\Gamma \vdash^{can} M : S$ presented in §3.5, except for the projection rule which takes an additional premise checking for anchorability of the resulting signature. All *anchorable typing* derivations can be translated into source typing derivations.

<footnote n="1">¹Adding a type field for *t* would not work, as it would not be an equivalent signature.</footnote>
<figure><img src="image_55.png" /><figcaption>Canonical signature $S_1$ Source signature $S_1$</figcaption></figure>

<figure><img src="image_56.png" /><figcaption>Canonical signature $S_2$ Source signature $S_2$</figcaption></figure>

Example 5: Graphical representation of the anchoring process on the type sharing trees. In the two canonical signatures $S_1$ and $S_2$, the existential type $\alpha$ is anchorable. For $S_1$, we can use $X.t$ for the handle to $\alpha$, as done in $S_1$. For $S_2$, a projection removed $X.t$ and $X.u$. The handle becomes $Y.a$ as shown in $S_2$.

**Theorem 2** (Anchorable typing). Anchorable typing produces a signature that is valid regarding the source typing rules:

$$ \Gamma \vdash^{anc} M : S \quad \wedge \quad \Gamma \vdash^{anc} S \hookrightarrow \Gamma_s; \theta_{\Gamma} \vdash S : \theta \quad \Rightarrow \quad \Gamma_s \vdash^{src} M : S \qquad (6) $$

More explanations and the formal definition of the anchoring process are given in §A. This completes the link between the source and canonical systems: canonical derivations can be translated back into the source when we restrict their expressiveness. The last link, namely the actual encoding in $F^\omega$ that inspired the design of the canonical system, is detailed in §B.

## Conclusion

ML-Module systems are known for being a well-studied but complex topic. The path-based, OCAML approach has proven to be successful in practice, but has some structural issues. While being restricted to a generative subset, our study of the signature avoidance problem in the source presentation exposes the limitations of the current signature syntax. These limitations are at the heart of the need for *ad-hoc* and complex fixes (strengthening, equivalence). Building on previous works, we introduced the canonical system as a more expressive yet simpler language, equipped with the right construction (existential types) to separate quantification and structural information, and solve the main issues of the source system. Using the canonical system, we shined a new light on the ad-hoc techniques of the source presentation and provided a detailed description of the solvable and unsolvable cases of signature avoidance. While still being close to the OCAML source, the canonical presentation can easily be elaborated into $F^\omega$, which provides formal guarantees. As a middle-point between usability and formalism, the canonical system is both a comprehensive description and a framework for building new features and improving the algorithms (specifically for the *solvable* cases of signature avoidance) of the current OCAML typechecker.

## References

K. Crary. A focused solution to the avoidance problem. *Journal of Functional Programming*, 30: e24, 2020. ISSN 0956-7968, 1469-7653. doi: 10.1017/S0956796820000222. URL https://www.cambridge.org/core/product/identifier/S0956796820000222/type/journal_article.
D. DREYER. Recursive type generativity. *Journal of Functional Programming*, 17(4-5): 433-471, 2007. doi: 10.1017/S0956796807006429.

R. Harper and M. Lillibridge. A type-theoretic approach to higher-order modules with sharing. In *Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, POPL '94, page 123-137, New York, NY, USA, 1994. Association for Computing Machinery. ISBN 0897916360. doi: 10.1145/174675.176927. URL https://doi.org/10.1145/174675.176927.

R. Harper, J. C. Mitchell, and E. Moggi. Higher-order modules and the phase distinction. In *Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, POPL '90, page 341-354, New York, NY, USA, 1989. Association for Computing Machinery. ISBN 0897913434. doi: 10.1145/96709.96744. URL https://doi.org/10.1145/96709.96744.

X. Leroy. Manifest types, modules, and separate compilation. In *Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, POPL '94, page 109-122, New York, NY, USA, 1994. Association for Computing Machinery. ISBN 0897916360. doi: 10.1145/174675.176926. URL https://doi.org/10.1145/174675.176926.

X. Leroy. Applicative functors and fully transparent higher-order modules. In *Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '95*, pages 142-153, San Francisco, California, United States, 1995. ACM Press. ISBN 978-0-89791-692-9. doi: 10.1145/199448.199476. URL http://portal.acm.org/citation.cfm?doid=199448.199476.

X. Leroy. A modular module system. *J. Funct. Program.*, 10(3):269-303, 2000. URL http://journals.cambridge.org/action/displayAbstract?aid=54525.

D. B. MacQueen. *Using Dependent Types to Express Modular Structure*, page 277-286. Association for Computing Machinery, New York, NY, USA, 1986. ISBN 9781450373470. URL https://doi.org/10.1145/512644.512670.

A. Madhavapeddy, R. Mortier, C. Rotsos, D. J. Scott, B. Singh, T. Gazagnaire, S. Smith, S. Hand, and J. Crowcroft. Unikernels: library operating systems for the cloud. In V. Sarkar and R. Bodík, editors, *Architectural Support for Programming Languages and Operating Systems*, ASPLOS 2013, Houston, TX, USA, March 16-20, 2013, pages 461-472. ACM, 2013. doi: 10.1145/2451116.2451167. URL https://doi.org/10.1145/2451116.2451167.

J. C. Mitchell and G. D. Plotkin. Abstract types have existential types. In *Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages*, POPL '85, page 37-51, New York, NY, USA, 1985. Association for Computing Machinery. ISBN 0897911474. doi: 10.1145/318593.318606. URL https://doi.org/10.1145/318593.318606.

B. Montagu and D. Rémy. Modeling Abstract Types in Modules with Open Existential Types. In *Proceedings of the 36th ACM Symposium on Principles of Programming Languages (POPL'09)*, pages 354-365, Savannah, GA, USA, Jan. 2009. ISBN 978-1-60558-379-2. doi: http://doi.acm.org/10.1145/1480881.1480926.

G. Radanne, T. Gazagnaire, A. Madhavapeddy, J. Yallop, R. Mortier, H. Mehnert, M. Perston, and D. Scott. Programming unikernels in the large via functor driven development, 2019.
A. Rossberg. 1ML - Core and modules united. *J. Funct. Program.*, 28:e22, 2018. doi: 10.1017/S0956796818000205. URL https://doi.org/10.1017/S0956796818000205.

A. Rossberg, C. Russo, and D. Dreyer. F-ing modules. *Journal of Functional Programming*, 24(5):529-607, Sept. 2014. ISSN 0956-7968, 1469-7653. doi: 10.1017/S0956796814000264. URL https://www.cambridge.org/core/product/identifier/S0956796814000264/type/journal_article.

C. V. Russo. Types for modules. *Electronic Notes in Theoretical Computer Science*, 60:3-421, 2004. ISSN 1571-0661. doi: https://doi.org/10.1016/S1571-0661(05)82621-0. URL https://www.sciencedirect.com/science/article/pii/S1571066105826210.

L. White, F. Bour, and J. Yallop. Modular implicits. In *Proceedings ML Family/OCaml Users and Developers workshops, ML/OCaml 2014, Gothenburg, Sweden, September 4-5, 2014.*, pages 22-63, 2014. doi: 10.4204/EPTCS.198.2. URL https://doi.org/10.4204/EPTCS.198.2.
# A Anchoring

## A.1 Anchoring of signatures

In this section we present in more details the mechanism that, under certain conditions, allows to build one of the source signatures corresponding to a given canonical signature. As mentioned in §4.2, the anchoring judgment, written

$$ \Gamma \vdash_S^{anc} S \leftrightarrow \Gamma_s; \theta_\Gamma \vdash S : \theta $$

states that, given a canonical signature $S$ and environment $\Gamma$, we can build a corresponding source signature $S$ and source environment $\Gamma_s$. Both are returned with an *anchoring map* $(\theta$ for the signature and $\theta_\Gamma$ for the environment) that gives a path $Q.t$ for the handle of every abstract type $\alpha$.

The anchoring map is extended when a type declaration with an *un-mapped* existential is encountered, which can be seen in rule C-ACH-DECL-ANCHORPOINT: the anchoring of the type declaration returns a non-empty map $\alpha \mapsto t$. In contrast, if the type field is concrete, an empty anchoring map is produced, as in Rule C-ACH-DECL-TYPE. Maps are merged together with the sequence rule C-ACH-DECL-SEQ, via the merging operator $\uplus$. The map associated with the left-hand-side declaration is *prefixed* with the self-reference. More generally, we write $Q.\theta$ as a shortcut for the map $\alpha \mapsto Q.\theta(\alpha)$.

### C-ACH-DECL-ANCHORPOINT

$$ \Gamma \leftrightarrow \Gamma_s : \theta_\Gamma \qquad \alpha \notin \text{dom}(\theta_\Gamma) $$

$$ \Gamma \vdash_A^{anc} \text{ type } t = \alpha \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \text{ type } t = A.t : (\alpha \leftrightarrow t) $$

### C-ACH-DECL-TYPE

$$ \Gamma \vdash^{anc} \tau \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \tau' : \emptyset $$

$$ \Gamma \vdash_A^{anc} \text{ type } t = \tau \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \text{ type } t = \tau' : \emptyset $$

### C-ACH-DECL-SEQ

$$ \Gamma \vdash^{anc} D \leftrightarrow \Gamma_s; \theta_\Gamma \vdash D : \theta \qquad \Gamma \vdash^{anc} \bar{D} \leftrightarrow (\Gamma_s, A.I : D); (\theta_\Gamma \uplus A.\theta) \vdash \bar{D} : \theta' $$

$$ \Gamma \vdash_A^{anc} D, \bar{D} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash D, \bar{D} : \theta_\Gamma \uplus \theta' $$

The judgment is easily extended to signatures and environments. Rule C-ACH-ENV-DECL shows how the anchoring map associated with a single declaration is merged with the environment map.

### C-ACH-ENV-DECL

$$ \Gamma \leftrightarrow \Gamma_s : \theta_\Gamma \qquad \Gamma, \bar{\alpha} \vdash_A^{anc} D \leftrightarrow \Gamma_s; \theta_\Gamma \vdash D : \theta \qquad \text{dom}(\theta) = \bar{\alpha} $$

$$ \Gamma, \bar{\alpha}, A.I : D \leftrightarrow (\Gamma_s, A.I : D) : \theta_\Gamma \uplus A.\theta $$

## A.2 Anchorable typing

As mentioned in §4.2, we can use the anchoring judgment to restrict the canonical typing to anchorable signatures. In our approach, the only place where a *non-anchorable* signature can be introduced is during projection on a submodule. Thus, we reuse all the rules of §3.5, except for the projection rule, which is modified to force the resulting signature to be anchorable:

### C-TYPA-MOD-PROJ

$$ \Gamma \vdash M : \exists \bar{\alpha}. \text{sig}_A \bar{D}_1, \text{module } X : \mathcal{R}, \bar{D}_2 \text{ end} \qquad \Gamma \vdash^{anc} \exists \bar{\alpha}. \mathcal{R} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash S : \theta $$

$$ \Gamma \vdash^{anc} M.X : \exists \bar{\alpha}. \mathcal{R} $$
As expected, the anchorable typing, as a restriction of the canonical typing to source-only mechanisms, respects the source typing. More formally:

**Theorem 3** (Anchorable typing). Given any environment $\Gamma$, module $M$ and (canonical) signature $S$, the anchored signature $S$ is a valid signature for the source typing:

$$ \left. \begin{array}{l} \Gamma \vdash^{\text{anc}} M : S \\ \Gamma \vdash^{\text{anc}} S \leftrightarrow \Gamma_s ; \theta_{\Gamma} \vdash S : \theta \end{array} \right\} \Rightarrow \Gamma_s \vdash^{\text{src}} M : S \qquad (7) $$

The proof of this theorem uses the following lemma :

**Lemma 1** (Anchorability of subtyping). Given $\Gamma$, $\Gamma_s$, $\sigma_\Gamma$, two canonical signatures $S_1$ and $S_2$, two source signatures $S_1$ and $S_2$, and two substitutions $\sigma_1$ and $\sigma_2$, we have:

$$ \left. \begin{array}{l} \Gamma \vdash^{\text{anc}} S \leftrightarrow \Gamma_s ; \theta_{\Gamma} \vdash S : \theta \\ \Gamma \vdash^{\text{anc}} S' \leftrightarrow \Gamma_s ; \theta_{\Gamma} \vdash S' : \theta' \\ \Gamma \vdash^{\text{can}} S < : S' \end{array} \right\} \Rightarrow \Gamma_s \vdash^{\text{src}} S < : S' \qquad (8) $$

This completes the presentation of the link between the source and the canonical systems. As mentioned, the canonical system was designed as a simpler presentation of the mechanisms found in the $F^\omega$ encoding of modules. To complete this presentation, the next section gives in more details the encoding and the main techniques used, especially regarding the sharing of abstract types.

# B $F^\omega$ and elaboration

To properly finish the transition from source to $F^\omega$ via the canonical system, we are missing one final link from the canonical system to $F^\omega$. In this section we give formal foundations and guarantees for the canonical system through elaboration into $F^\omega$: the elaboration is defined by hybrid judgments that relate module expressions and canonical signatures to terms and types of $F^\omega$. This gives a precise correspondence between the key mechanisms of the canonical system, in particular existential types, and standard mechanisms of $F^\omega$. The canonical system can actually be understood as a particular mode of use of $F^\omega$. Thanks to $F^\omega$, elaborated terms enjoy the properties of soundness, progress, and type preservation. In fact, the canonical system has been designed with the elaboration in mind, mainly by erasing proof terms and only retaining $F^\omega$ types. Hence, the elaboration is mostly straightforward.

Although, we use $F^\omega$ as the target language, we do not actually need the power of $F^\omega$ to model generative functors. The reason to pursue the development in $F^\omega$ is to also allow parameterized types in the source language and to be able to extend the encoding to the case of applicative functors in the future.

We start by giving the syntax and rules of the version of $F^\omega$ (extended with existential types and records) that we use for the elaboration and present the $F^\omega$ terms and types that encode modules and signatures. Then, we introduce the hybrid judgments. Finally, we state the correctness theorem for the elaboration and the link between the canonical system and $F^\omega$.

This section is largely inspired by Rossberg et al. [2014]. We only made minor changes to the encoding of module expressions and signatures: the encoding of module types use $\lambda$-abstraction rather than existential quantification; declarations are encoded differently. The main difference is the extension of the judgments to produce both the $F^\omega$ type and the canonical signature, whereas in Rossberg et al. [2014], typing and subtyping are only defined by elaboration.
$$ \kappa := \Omega \mid \kappa \to \kappa \qquad \text{(kinds)} $$

$$ \rho := \alpha \mid \rho \to \rho \mid \{\overline{\ell} : \rho\} \mid \forall \alpha : \kappa.\rho \mid \exists \alpha : \kappa.\rho \mid \lambda \alpha : \kappa.\rho \mid \rho \rho \qquad \text{(types)} $$

$$ \begin{align*} E := & x \mid \lambda x : \rho.E \mid E E \mid \{\overline{\ell = E}\} \mid E.\ell \mid \lambda \alpha : \kappa.E \mid E \rho \\ & \mid \mathit{pack} \langle \rho, E \rangle_{\rho} \mid \mathit{unpack} \langle \alpha, x \rangle = E \text{ in } E \tag*{\text{(terms)}} \end{align*} $$

$$ W := \lambda x : \rho.E \mid \{\overline{\ell = W}\} \mid \lambda \alpha : \kappa.E \mid \mathit{pack} \langle \rho, W \rangle_{\rho} \qquad \text{(values)} $$

$$ \Gamma := \cdot \mid \Gamma, \alpha : \kappa \mid \Gamma, x : \rho \qquad \text{(environments)} $$

<table><caption>Figure 6: Syntax of $F^\omega$</caption><tr><td colspan="2"><strong>Abstract signature</strong></td><td colspan="2"><strong>Declaration (with syntactic sugar)</strong></td></tr><tr><td>$\Pi := \exists \overline{\alpha}.\Sigma$</td><td>$\zeta := \text{val } x : \rho$</td><td>$\triangleq \ell_x : \rho$</td><td>(Value)</td></tr><tr><td colspan="2"><strong>Concrete signature</strong></td><td>$\mid \text{type } t = \rho$</td><td>$\triangleq \ell_t : \langle\langle\rho\rangle\rangle$</td><td>(Type)</td></tr><tr><td>$\Sigma := \forall \overline{\alpha}.\Sigma \to \Pi$ (Functor)</td><td>$\mid \text{module } X : \Sigma$</td><td>$\triangleq \ell_X : \Sigma$</td><td>(Module)</td></tr><tr><td>$\mid \{\overline{\zeta}\}$ (Signature)</td><td>$\mid \text{module type } T = \lambda \overline{\alpha}.\Sigma$</td><td>$\triangleq \ell_T : \langle\langle\lambda \overline{\alpha}.\Sigma\rangle\rangle$</td><td>(Module type)</td></tr></table>

<caption>Figure 7: Syntactic categories and encoding</caption>

## B.1 F-omega and encoded signatures

We use a standard variant of explicitly typed $F^\omega$ with primitive records and existential types; We only give its syntax in Figure 6; its typing rules are available in §E. We use letters $\rho$ and $E$ to range over types and expressions so as to distinguish them from the core language types and expressions, $\tau$ and $e$, although these should be seen as a subset of $\rho$ and $E$. While kinds are part of terms, we usually omit them in $F^\omega$ terms for the sake of conciseness and readability.

To help with the elaboration, we assume a collection $\ell_I$ of record labels indexed by identifiers of the canonical (and source) system. The encoding of the canonical system into $F^\omega$ is described in Figure 7. Functors are encoded as functions and structural signatures as records. Declarations are encoded as record entries: we use the category of the identifier to distinguish between the encoding of values, types, modules and module types. We also introduce some syntactic sugar to have the encoding of declarations look similar to the usual canonical and source syntax. We use the following (overloaded) operator to shorten the encoding of type and module-type fields, with the type encoding on the left and the corresponding term on the right:

$$ \langle\langle\rho\rangle\rangle := \forall (\beta : \kappa \to \star). \beta \rho \to \beta \rho \quad \text{(Type)} \qquad \langle\langle\rho\rangle\rangle := \Lambda(\beta : \kappa \to \star). \lambda(x : \beta \rho). x \quad \text{(Term)} $$

This allows to represent *type fields* as $F^\omega$ terms, specifically record fields: the term is always the identity and only its type encoding in the annotation matters, namely to enforce typing constraints. Indeed, erasing type fields during elaboration would have been possible, but this would prevent the elaboration from distinguishing canonical terms that would only differ from their type fields. This will ensure that two modules that differ only from their type definitions (i.e., their type fields) will also differ in their signatures. The type is generalized with a type operator $\beta$ to allow the encoding of higher-kinded types.

A representative example of the encoding of a simple module is given in Example 6. The encoded signature is a type of $F^\omega$ that can be read as a canonical signature. Using the syntactic sugar makes the similarity with the source type even more striking. In the evidence term, we can see that the sealing of `int` corresponds to a `pack(int, ...)` term. To share the abstract type between the two fields (`X` and `u`), the abstract type is unpacked and then repacked, using a
pattern of the form unpack<α, ·> = · in pack<α, ·> called a repacking pattern.

1
module M = struct
  module X = (struct
    type t = int
    let v = 42
  end : sig
    type t
    val v : t
end)

module U = X.t*bool

module V = (struct
  type u = U.t*bool
end)

### Encoded signature

$$ \Pi = \exists \alpha \left\{ \begin{array}{l} \ell_X : \{ \ell_t : \langle\langle \alpha \rangle\rangle \} \\ \ell_v : \alpha \\ \ell_u : \langle\langle \alpha \times \mathbf{bool} \rangle\rangle \end{array} \right\} \triangleq \exists \alpha \left\{ \begin{array}{l} \text{module } X : \left\{ \begin{array}{l} \text{type } t = \alpha \\ \text{val } v : \alpha \end{array} \right\} \\ \text{type } u = \alpha \times \mathbf{bool} \end{array} \right\} $$

### Encoded module

$$ \begin{align*} E = \mathit{unpack}(\alpha_1, y_1) &= \mathit{pack}(\mathit{int}, \{\ell_X = \{\ell_t = \langle\langle \mathit{int} \rangle\rangle, \ell_v = 42\}\}) \text{ in} \\ \mathit{unpack}(\emptyset, y_2) &= \{\ell_u = \langle\langle (\alpha_1 \times \mathbf{bool}) \rangle\rangle\} \text{ in} \\ \mathit{pack}(\alpha_1, \{\ell_X = (y_1.\ell_X), \ell_u = (y_2.\ell_u)\}) &\end{align*} $$

Example 6: A simple module with two components (a submodule X and a type definition u). Its signature is encoded into a type Π of $F^ω$. A term E (called an *evidence term*) represents the module and has type Π.

## B.2 An extension of the canonical system

The *hybrid* system can be seen as an *extension* of the canonical one: the judgments are extended to actually present both the canonical and $F^ω$ parts. We define all judgments over an extended, hybrid environment $\Delta$ that contains both canonical and $F^ω$ terms, defined as follows:

$$ \Delta ::= \emptyset \mid \Delta, \bar{\alpha} \mid \Delta, (Y : (\mathcal{R}, \Sigma)) \mid \Delta, (A.I : (\mathcal{D}, \zeta)) $$

The elaborated judgments rely on a core-language translation into $F^ω$ for terms and types, that is omitted here.

### B.2.1 Subtyping

We define the subtyping judgment $\Delta \vdash_S \mathcal{S}_1 <: \mathcal{S}_2 \rightsquigarrow \Pi_1 <: \Pi_2 \Rightarrow f$, which follows closely the canonical one, as the handling of canonical signatures and $F^ω$ types are similar. We use a version of $F^ω$ with explicit subtyping, so the judgment is extended to produce a *subtyping function* $f: \Pi_1 \to \Pi_2$. The nature of this subtyping function gives interesting insights on the compilation of modules. For abstraction-only subtyping, the subtyping function is $\beta\eta$-convertible to the identity as the memory representation of modules (the terms) are the same when stripped of types. For general subtyping (with reordering or deletion of fields), the subtyping function is not *code-free*; correspondingly, it requires a specific action from the compiler (copy, access table, etc.).

The rule for functor subtyping **E-SUB-SIG-FUNCTOR** illustrates the main mechanisms: building on the subtyping functions (and type matching $\bar{\tau}$) for the parameter and the body, we craft a subtyping function from the left-hand-side functor signature to the right-hand-side one. All
the rules are given in §F.1.

E-SUB-SIG-FUNCTOR

$$
\begin{align*}
\Delta, \bar{\alpha}' \vdash_{\text{elab}} \mathcal{R}'_a &:= \mathcal{R}_a[\bar{\alpha} \mapsto \bar{\tau}] \rightsquigarrow \Sigma'_a &<: \Sigma_a[\bar{\tau} \mapsto \bar{\alpha}] &\Rightarrow f_a \\
\Delta, \bar{\alpha}', (Y : (\mathcal{R}'_a, \Sigma'_a)) \vdash_{\text{elab}} \mathcal{S}[\bar{\alpha} \mapsto \bar{\tau}] &<: S' \rightsquigarrow \Pi[\bar{\alpha} \mapsto \bar{\tau}] &<: \Pi' &\Rightarrow f &\quad Y \notin \Delta \\
\Delta \vdash_{\text{elab}} \forall \bar{\alpha}. (Y : \mathcal{R}_a) &\rightarrow \mathcal{S} \quad<: \forall \bar{\alpha}'. (Y : \mathcal{R}'_a) &\rightarrow \mathcal{S}' \rightsquigarrow \forall \bar{\alpha}. \Sigma_a &\rightarrow \Pi \quad<: \forall \bar{\alpha}'. \Sigma'_a &\rightarrow \Pi' \\
&[\lambda(g : (\forall \bar{\alpha}. \Sigma_a \rightarrow \Pi)). \Lambda \bar{\alpha}'. \lambda(x : \Sigma'_a) . f(g \bar{\tau} (f_a x))] &
\end{align*}
$$

B.2.2 Typing

As for subtyping, the typing rules extend the canonical ones and produce an $F^\omega$ type (and term for module and bindings). When handling signatures and types, the lifting of existentials is just a rewriting. Producing the actual proof terms shows how the extension of scope is made using the repacking pattern. All the rules are given in §F.2.

**Binding typing rules** A binder is encoded with a single-field declaration record. The extrusion of existential types is illustrated in Rule **E-TYP-DECL-MOD**. In the sequence rule **E-TYP-DECL-SEQ**, two bindings are merged using a let-binding for renaming. The extension of scope needed to make the abstract types of the first declaration $\bar{\alpha}_1$ available to the rest also uses the repacking pattern.

E-TYP-DECL-MOD

$$
\begin{align*}
\Delta \vdash_{\text{elab}} M : & \exists \bar{\alpha}. \mathcal{R} \rightsquigarrow e : \exists \bar{\alpha}. \Sigma & A.X \notin \Delta \\
\Delta \vdash_{\text{A}}^{\text{elab}} (\text{module } X = M) : & (\exists \bar{\alpha}. \text{module } X : \mathcal{R}) \rightsquigarrow \begin{array}{l} \text{unpack}(\bar{\alpha}, y) = e \text{ in } \text{pack}(\bar{\alpha}, \{\ell_X = y\}) \\ \qquad : (\exists \bar{\alpha}. \text{module } X : \Sigma) \end{array}
\end{align*}
$$

E-TYP-DECL-SEQ

$$
\begin{align*}
\Delta \vdash_A^{\text{elab}} B_1 : & \exists \bar{\alpha}_1. \mathcal{D}_1 \rightsquigarrow e_1 : \exists \bar{\alpha}_1. \{\zeta_1\} & \Delta, \bar{\alpha}_1, A.I_1 : (\mathcal{D}_1, \zeta_1) \vdash_A^{\text{elab}} \bar{B} : & \exists \bar{\alpha}. \bar{\mathcal{D}} \rightsquigarrow e : \exists \bar{\alpha}. \{\bar{\zeta}\} \\
\Delta \vdash_A^{\text{elab}} B_1, \bar{B} : & \exists \bar{\alpha}_1 \bar{\alpha}. \bar{\mathcal{D}}_1, \bar{\mathcal{D}} \rightsquigarrow \begin{array}{@{}l@{}} \text{unpack}(\bar{\alpha}_1, x_1) = e_1 \text{ in} \\ \text{unpack}(\bar{\alpha}, x) = (\text{let } A.I_1 = x_1. \ell_{I_1} \text{ in } e) \text{ in} \\ \text{pack}(\bar{\alpha}_1 \bar{\alpha}, \{\ell_I = x_1. \ell_I, \ell_I = x. \ell_I\}) \end{array} & & \\
& : \exists \bar{\alpha}_1 \bar{\alpha}. \{\zeta_1, \bar{\zeta}\} & &
\end{align*}
$$

**Module expressions typing** We only present the key typing rules for module expressions. The introduction of abstract types is done by sealing (**E-TYP-MOD-SEALING**), and features an explicit isolated *packing* (as opposed to a repacking). The application of functor (**E-TYP-MOD-APP**) shows how the polymorphic interface (universally quantified) is instantiated with types (obtained from the matching of the argument's and parameter's signatures). Finally, the projection rule (**E-TYP-MOD-PROJ**) illustrates another usage of the repacking pattern to collect
abstract types, project on the X submodule, and put back the abstract types.

E-TYP-MOD-SEALING

$$ \Delta \vdash^{\text{elab}} S : \lambda \bar{\alpha}. \mathcal{R} \rightsquigarrow \lambda \bar{\alpha}. \Sigma \qquad \Delta \vdash^{\text{elab}} P : \mathcal{R}' \rightsquigarrow e : \Sigma' $$

$$ \Delta \vdash^{\text{elab}} \mathcal{R}' < : \mathcal{R}[\bar{\alpha} \mapsto \bar{\tau}] \rightsquigarrow \Sigma' < : \Sigma[\bar{\alpha} \mapsto \bar{\tau}] \Rightarrow f $$

$$ \Delta \vdash^{\text{elab}} (P : S) : \exists \bar{\alpha}. \mathcal{R} \rightsquigarrow \text{pack}(\bar{\tau}, (f e)) : \lambda \bar{\alpha}. \Sigma $$

E-TYP-MOD-APP

$$ \Delta \vdash^{\text{elab}} P' : \mathcal{R}' \rightsquigarrow e' : \Sigma' $$

$$ \Delta \vdash^{\text{elab}} P : \forall \bar{\alpha}. (Y : \mathcal{R}) \rightarrow S \rightsquigarrow e : \forall \bar{\alpha}. \Sigma \rightarrow S $$

$$ \Delta \vdash^{\text{elab}} \mathcal{R}' < : \mathcal{R}[\bar{\alpha} \mapsto \bar{\tau}] \rightsquigarrow \Sigma' < : \Sigma[\bar{\alpha} \mapsto \bar{\tau}] \Rightarrow f $$

$$ \Delta \vdash^{\text{elab}} P(P') : \mathcal{R}[\bar{\alpha} \mapsto \bar{\tau}] \rightsquigarrow e \bar{\tau} (f e') : \Pi[\bar{\alpha} \mapsto \bar{\tau}] $$

E-TYP-MOD-PROJ

$$ \Delta \vdash^{\text{elab}} M : \exists \bar{\alpha}. \text{sig}_A \bar{D}_1, \text{module } X : \mathcal{R}, \bar{D}_2 \text{ end} \rightsquigarrow e : \{\zeta_1, \ell_X : \Sigma, \zeta_2\} $$

$$ \Delta \vdash^{\text{elab}} M.X : \exists \bar{\alpha}. \mathcal{R} \rightsquigarrow \text{unpack}(\bar{\alpha}, y) = e \text{ in } \text{pack}(\bar{\alpha}, e.\ell_X) : \exists \bar{\alpha}. \Sigma $$

## B.3 Correctness and link with the canonical system

We write $\Delta^{\text{can}}$ and $\Delta^{\text{F}}$ for the left and right projections of the hybrid context $\Delta$, defined in the obvious way. We present implications as rules.

**Theorem 4** (Correctness of elaboration). The elaboration judgment ensures well-typedness on both sides. For subtyping, we have the following result:

$$ \Delta \vdash^{\text{elab}} S < : S' \rightsquigarrow \Pi < : \Pi' \Rightarrow f \Rightarrow \left\{ \begin{array}{l} \Delta^{\text{F}} \vdash^{\text{can}} S < : S' \\ \Delta^{\text{F}} \vdash f : \Pi \rightarrow \Pi' \end{array} \right. \qquad (9) $$

For typing, we have the following result:

$$ \Delta \vdash^{\text{elab}} M : S \rightsquigarrow e : \Pi \Rightarrow \left\{ \begin{array}{l} \Delta^{\text{can}} \vdash^{\text{can}} M : S \\ \Delta^{\text{F}} \vdash e : \Pi \end{array} \right. \qquad (10) $$

Conversely, we show that well-typedness in the canonical system ensures that elaboration is well-defined. We first observe that there is an isomorphism between canonical and $F^{\omega}$-encoded signatures. This allows us, for a given signature $S$ (resp. $\mathcal{R}$) to consider its encoding in $F^{\omega}$, noted $\Pi_S$ (resp. $\Sigma_{\mathcal{R}}$). Similarly, we may consider the extension of an environment $\Gamma$ into a hybrid enriched environment $\Delta_{\Gamma}$ (we omit the definition.)

**Theorem 5** (Enrichment of canonical judgments). The $F^{\omega}$ terms $(e, f, \Pi_S)$ corresponding to canonical derivation always exist. More formally, we have:

$$ \Gamma \vdash^{\text{can}} S : S \Rightarrow \Delta_{\Gamma} \vdash^{\text{elab}} S : S \rightsquigarrow \Pi_S \qquad (11) $$

$$ \Gamma \vdash^{\text{can}} S_1 < : S_2 \Rightarrow \exists f, \Delta_{\Gamma} \vdash^{\text{elab}} S_1 < : S_2 \rightsquigarrow \Pi_{S_1} < : \Pi_{S_2} \Rightarrow f \qquad (12) $$

$$ \Gamma \vdash^{\text{can}} M : S \Rightarrow \exists e, \Delta_{\Gamma} \vdash^{\text{elab}} M : S \rightsquigarrow e : \Pi_S \qquad (13) $$

# C Source system – Complete rules

## C.1 Resolution

### C.1.1 $\Gamma \vdash P \triangleright S$ – Path resolution
$$ \frac{\text{S-RES-LOCALMOD}}{\Gamma \vdash A.X \triangleright S} \quad (A.X : S) \in \Gamma $$

$$ \frac{\text{S-RES-FCTARG}}{\Gamma \vdash Y \triangleright S} \quad (Y : S) \in \Gamma $$

$$ \frac{\text{S-RES-PROJ-MOD}}{\Gamma \vdash P \triangleright \text{sig}_A \bar{D} \text{ end}} \quad (\text{module } X : S) \in \bar{D} $$

$$ \frac{\text{S-RES-MODTYPE}}{\Gamma \vdash P \triangleright S} \quad \frac{\Gamma \vdash P \triangleright Q.T \quad \Gamma \vdash Q.T \triangleleft S}{\Gamma \vdash P \triangleright S} $$

### C.1.2 $\Gamma \overset{\text{src}}{\vdash} S \triangleleft S' - \text{Signature resolution}$

$$ \frac{\text{S-RES-LOCALSIG}}{\Gamma \vdash A.T \triangleleft S} \quad (A.T : S) \in \Gamma $$

$$ \frac{\text{S-RES-PROJ-MODTYPE}}{\Gamma \vdash P \triangleright \text{sig}_A \bar{D} \text{ end}} \quad (\text{module type } T = S) \in \bar{D} $$

$$ \frac{\text{S-RES-MODTYPE-REC}}{\Gamma \vdash Q.T \triangleleft Q'.T' \quad \Gamma \vdash Q'.T' \triangleleft S} \quad \Gamma \vdash Q.T \triangleleft S $$

## C.2 Equivalence

### C.2.1 $\Gamma \overset{\text{src}}{\vdash} \tau \approx \tau' - \text{Type equivalence}$

$$ \frac{\text{S-EQV-TYPE-LOCAL}}{\Gamma \vdash A.t \approx \tau} \quad (A.t : \text{type } t = \tau) \in \Gamma $$

$$ \frac{\text{S-EQV-TYPE-RES}}{\Gamma \vdash P \triangleright \text{sig}_A \bar{D} \text{ end}} \quad (\text{type } t = \tau) \in \bar{D} $$

$$ \frac{\text{S-EQV-TYPE-TRANS}}{\Gamma \overset{\text{src}}{\vdash} \tau_1 \approx \tau_2 \quad \Gamma \overset{\text{src}}{\vdash} \tau_2 \approx \tau_3} \quad \Gamma \overset{\text{src}}{\vdash} \tau_1 \approx \tau_3 $$

$$ \frac{\text{S-EQV-TYPE-SYM}}{\Gamma \overset{\text{src}}{\vdash} \tau' \approx \tau} \quad \Gamma \overset{\text{src}}{\vdash} \tau \approx \tau' $$

$$ \frac{\text{S-EQV-TYPE-REFL}}{\Gamma \overset{\text{src}}{\vdash} \tau \approx \tau} $$

### C.2.2 $\Gamma \overset{\text{src}}{\vdash} A \quad D \approx D' - \text{Declaration equivalence}$
S-EQV-DECL-VAL

$$ \frac{\Gamma \vdash^{\text{src}} \tau \approx \tau'}{\Gamma \vdash_A (\text{val } x : \tau) \approx (\text{val } x : \tau')} $$

S-EQV-DECL-TYPE

$$ \frac{\Gamma \vdash^{\text{src}} \tau \approx \tau'}{\Gamma \vdash_A (\text{type } t = \tau) \approx (\text{type } t = \tau')} $$

S-EQV-DECL-MOD

$$ \frac{\Gamma \vdash^{\text{src}} S \approx S'}{\Gamma \vdash_A (\text{module } X : S) \approx (\text{module } X : S')} $$

S-EQV-DECL-MODTYPE

$$ \frac{\Gamma \vdash^{\text{src}} S \approx S'}{\Gamma \vdash_A (\text{module type } T = S) \approx (\text{module type } T = S')} $$

S-EQV-DECL-EMPTY

$$ \Gamma \vdash^{\text{src}} \emptyset \approx \emptyset $$

S-EQV-DECL-SEQ

$$ \frac{\Gamma \vdash_A D_1 \approx D'_1 \quad \Gamma, A.I_1 : D_1 \vdash_A \bar{D} \approx \bar{D'}}{\Gamma \vdash_A D_1, \bar{D} \approx D'_1, \bar{D'}} $$

### C.2.3 $\Gamma \vdash^{\text{src}} S \approx S'$ – Signature equivalence

S-EQV-SIG-MODTYPE

$$ \frac{\Gamma \vdash^{\text{src}} Q.T \Leftrightarrow S}{\Gamma \vdash^{\text{src}} Q.T \approx S} $$

S-EQV-SIG-FUNCTOR

$$ \frac{\Gamma \vdash^{\text{src}} S_a \approx S'_a}{\Gamma, Y : S_a \vdash^{\text{src}} S \approx S'} \qquad \Gamma \vdash^{\text{src}} (Y : S_a) \rightarrow S \approx (Y : S'_a) \rightarrow S' $$

S-EQV-SIG-SIG

$$ \frac{\Gamma \vdash_A \bar{D} \approx \bar{D'}}{\Gamma \vdash^{\text{src}} \text{sig}_A \bar{D} \text{ end} \approx \text{sig}_A \bar{D'} \text{ end}} $$

S-EQV-SIG-TRANS

$$ \frac{\Gamma \vdash^{\text{src}} S \approx S'}{\Gamma \vdash^{\text{src}} S' \approx S''} \qquad \frac{\Gamma \vdash^{\text{src}} S \approx S''}{\Gamma \vdash^{\text{src}} S \approx S} $$

S-EQV-SIG-REFL

$$ \Gamma \vdash^{\text{src}} S \approx S $$

S-EQV-SIG-SYM

$$ \frac{\Gamma \vdash^{\text{src}} S' \approx S}{\Gamma \vdash^{\text{src}} S \approx S'} $$

## C.3 Strengthening

### C.3.1 $\Gamma \vdash S/P \gg S'$ – Signature strengthening

S-STR-SIG-FUNCTOR

$$ \Gamma \vdash (Y : S_a) \rightarrow S/P \gg (Y : S_a) \rightarrow S $$

S-STR-SIG-SIG

$$ \frac{\Gamma \vdash \bar{D}[A \mapsto P]/P \gg \bar{D'}}{\Gamma \vdash \text{sig}_A \bar{D} \text{ end}/P \gg \text{sig}_A \bar{D'} \text{ end}} $$

### C.3.2 $\Gamma \vdash D/P \gg D'$ – Declaration strengthening
S-STR-DECL-VAL

$$ \Gamma \vdash \text{val } x : \tau / P \gg \text{val } x : \tau $$

S-STR-DECL-TYPE

$$ \Gamma \vdash \text{type } t = \tau / P \gg \text{type } t = \tau $$

S-STR-DECL-MOD

$$ \frac{\Gamma \vdash S / (P \cdot X) \gg S'}{\Gamma \vdash (\mathit{module} \ X : S) / P \gg \mathit{module} \ X : S'} $$

S-STR-DECL-MODTYPE

$$ \Gamma \vdash \mathit{module} \ \mathit{type} \ T = S / P \gg \mathit{module} \ \mathit{type} \ T = S $$

## C.4 Subtyping

Rules for both general and abstraction subtyping are shown, $<$: being either $<$: or $<>$:

### C.4.1 $\Gamma \upharpoonright_S S <: S' - \text{Signature subtyping}$

S-SUB-SIG-EQUIV

$$ \frac{\Gamma \vdash S \approx S'}{\Gamma \vdash S <: S'} $$

S-SUB-SIG-TRANS

$$ \frac{\Gamma \vdash S <: S' \qquad \Gamma \vdash S' <: S''}{\Gamma \vdash S <: S''} $$

S-SUB-SIG-FUNCTOR

$$ \frac{\Gamma \vdash S_a' <: S_a \qquad \Gamma, Y : S_a' \vdash S <: S' \qquad Y \notin \Gamma}{\Gamma \vdash (Y : S_a) \to S <: (Y : S_a') \to S'} $$

S-SUB-SIG-SIG

$$ \frac{\bar{D}_0 \subseteq \bar{D} \qquad \Gamma, \bar{A} \cdot \bar{D} \vdash_A^{\text{src}} \bar{D}_0 <: \bar{D}'}{\Gamma \vdash^{\text{src}} \mathit{sig}_A \quad \bar{D} \ \mathit{end} <: \ \mathit{sig}_A \quad \bar{D}' \ \mathit{end}} $$

S-SUBEQ-SIG-SIG

$$ \frac{\Gamma, \bar{A} \cdot \bar{D} \vdash \bar{D} <: \bar{D}'}{\Gamma \vdash^{\text{src}} \mathit{sig}_A \quad \bar{D} \ \mathit{end} <: \ \mathit{sig}_A \quad \bar{D}' \ \mathit{end}} $$

### C.4.2 $\Gamma \upharpoonright_A^\text{src} D <: D' - \text{Declaration subtyping}$

S-SUB-DECL-VAL

$$ \frac{\Gamma \vdash \tau \approx \tau'}{\Gamma \vdash_A^\text{src} (\text{val } x : \tau) <: (\text{val } x : \tau')} $$

S-SUB-DECL-TYPE

$$ \frac{\Gamma \vdash \tau \approx \tau'}{\Gamma \vdash_A^\text{src} (\text{type } t = \tau) <: (\text{type } t = \tau')} $$

S-SUB-DECL-MOD

$$ \frac{\Gamma \vdash S <: S'}{\Gamma \vdash_A^\text{src} (\mathit{module} \ X : S) <: (\mathit{module} \ X : S')} $$

S-SUB-DECL-MODTYPE

$$ \frac{\Gamma \vdash S <: S' \qquad \Gamma \vdash S' <: S}{\Gamma \vdash_A^\text{src} (\mathit{module} \ \mathit{type} \ T = S) <: (\mathit{module} \ \mathit{type} \ T = S')} $$
## C.5 Typing

### C.5.1 $\Gamma \vdash_S : \checkmark$ – Signature typing

S-TYP-SIG-LOCALMODTYPE

$$ \Gamma \vdash_{\text{src}} P.T : \text{sig}_A \bar{D} \text{ end} \qquad \text{module type } T = S \in \bar{D} $$

$$ \Gamma \vdash_{\text{src}} P.T : \checkmark $$

S-TYP-SIG-MODTYPE

$$ A.T : \text{module type } T = S \in \Gamma $$

$$ \Gamma \vdash_{\text{src}} A.T : \checkmark $$

S-TYP-SIG-FUNCTOR

$$ \Gamma \vdash_{\text{src}} S_a : \checkmark \qquad \Gamma, Y : S_a \vdash_{\text{src}} S : \checkmark \qquad Y \notin \Gamma $$

$$ \Gamma \vdash_{\text{src}} (Y : S_a) \rightarrow S : \checkmark $$

S-TYP-SIG-SIG

$$ \Gamma \vdash_{A} \bar{D} : \checkmark \qquad A \notin \Gamma $$

$$ \Gamma \vdash_{\text{src}} \text{sig}_A \bar{D} \text{ end} : \checkmark $$

### C.5.2 $\Gamma \vdash_A^S D : \checkmark$ – Declarations typing

S-TYP-DECL-VAL

$$ \Gamma \vdash_{\text{src}} \tau : \checkmark \qquad A.x \notin \Gamma $$

$$ \Gamma \vdash_{\text{src}}^S (\text{val } x : \tau) : \checkmark $$

S-TYP-DECL-TYPE

$$ \Gamma \vdash_{\text{src}} \tau : \checkmark \qquad A.t \notin \Gamma $$

$$ \Gamma \vdash_{\text{src}}^S (\text{type } t = \tau) : \checkmark $$

S-TYP-DECL-TYPEABS

$$ A.t \notin \Gamma $$

$$ \Gamma \vdash_{A}^{\text{src}} (\text{type } t = A.t) : \checkmark $$

S-TYP-DECL-MOD

$$ \Gamma \vdash_S : \checkmark \qquad A.X \notin \Gamma $$

$$ \Gamma \vdash_A^S (\text{module } X : S) : \checkmark $$

S-TYP-DECL-MODTYPE

$$ \Gamma \vdash_S : \checkmark \qquad A.T \notin \Gamma $$

$$ \Gamma \vdash_A^S (\text{module type } T = S) : \checkmark $$

S-TYP-DECL-EMPTY

$$ \Gamma \vdash_A^{\text{src}} \emptyset : \checkmark $$

S-TYP-DECL-SEQ

$$ \Gamma \vdash_A^{\text{src}} D_1 : \checkmark \qquad \Gamma, A.I_1 : D_1 \vdash_A^{\text{src}} \bar{D} : \checkmark $$

$$ \Gamma \vdash_A^S (D_1, \bar{D}) : \checkmark $$

### C.5.3 $\Gamma \vdash \tau : \checkmark$ – Type checking

S-TYP-TYPE-LOCALTYPE

$$ A.t : \text{type } t = \tau \in \Gamma $$

$$ \Gamma \vdash_{\text{src}} A.t : \checkmark $$

S-TYP-TYPE-QUALIFIEDPATHTYPE

$$ \Gamma \vdash_P : \text{sig}_A \bar{D} \text{ end} \qquad \text{type } t = \tau \in \bar{D} $$

$$ \Gamma \vdash_P : P.t : \checkmark $$

### C.5.4 $\Gamma \vdash_M : S$ – Module typing
S-TYP-MOD-RES

$$ \frac{\Gamma \vdash_{\text{src}} P \triangleright S}{\Gamma \vdash_{\text{src}} P : S} $$

S-TYP-MOD-STRENGTHEN

$$ \frac{\Gamma \vdash_{\text{src}} P : S \qquad \Gamma \vdash S/P \gg S'}{\Gamma \vdash P : S'} $$

S-TYP-MOD-EQUIV

$$ \frac{\Gamma \vdash_{\text{src}} M : S \qquad \Gamma \vdash_{\text{src}} S \approx S'}{\Gamma \vdash M : S'} $$

S-TYP-MOD-SEALING

$$ \frac{\Gamma \vdash_{\text{src}} S : \checkmark \qquad \Gamma \vdash_{\text{src}} P : S' \qquad \Gamma \vdash_{\text{src}} S' < : S}{\Gamma \vdash_{\text{src}} (P : S) : S} $$

S-TYP-MOD-FUNCTOR

$$ \frac{\Gamma \vdash_{\text{src}} S_a : \checkmark \qquad \Gamma ; (Y : S_a) \vdash_{\text{src}} M : S \qquad Y \notin \Gamma}{\Gamma \vdash_{\text{src}} (Y : S_a) \to M : (Y : S_a) \to S'} $$

S-TYP-MOD-FCTAPP

$$ \frac{\Gamma \vdash_{\text{src}} P : (Y : S_a) \to S \qquad \Gamma \vdash_{\text{src}} P' : S'_a \qquad \Gamma \vdash_{\text{src}} S'_a < : S_a}{\Gamma \vdash_{\text{src}} P(P') : S[Y \mapsto P']$$

S-TYP-MOD-STRUCT

$$ \frac{\Gamma \vdash_{\text{A}} \overline{B} : \overline{D} \qquad A \notin \Gamma}{\Gamma \vdash_{\text{src}} \text{struct}_{\text{A}} \overline{B} \text{ end} : \text{sig}_{\text{A}} \overline{D} \text{ end}} $$

S-TYP-PROJ

$$ \frac{\Gamma \vdash_{\text{src}} M : \text{sig}_{\text{A}} (\overline{D_1}, \text{module } X : S, \overline{D_2}) \text{ end}}{\Gamma \vdash_{\text{src}} M.X : S'} $$

### C.5.5 $\Gamma \vdash_{\text{A}}^{\text{src}} B : D$ – Bindings typing

S-TYP-BIND-LET

$$ \frac{\Gamma \vdash_{\text{src}} e : \tau \qquad A.x \notin \Gamma}{\Gamma \vdash_{\text{src}} (\text{let } x = e) : (\text{val } x : \tau)} $$

S-TYP-BIND-TYPE

$$ \frac{\Gamma \vdash_{\text{src}} \tau : \checkmark \qquad A.t \notin \Gamma}{\Gamma \vdash_{\text{src}} (\text{type } t = \tau) : (\text{type } t = \tau)} $$

S-TYP-BIND-ABSTRACT

$$ \frac{A.t \notin \Gamma}{\Gamma \vdash_{\text{A}}^{\text{src}} (\text{type } t = A.t) : (\text{type } t = A.t)} $$

S-TYP-BIND-MOD

$$ \frac{\Gamma \vdash_{\text{M}}^{\text{src}} M : S \qquad A.X \notin \Gamma}{\Gamma \vdash_{\text{A}}^{\text{src}} (\text{module } X = M) : (\text{module } X : S)} $$

S-TYP-BIND-MODTYPE

$$ \frac{\Gamma \vdash_{\text{S}}^{\text{src}} S : \checkmark \qquad A.T \notin \Gamma}{\Gamma \vdash_{\text{A}}^{\text{src}} (\text{module type } T = S) : (\text{module type } T = S)} $$

S-TYP-BIND-EMPTY

$$ \Gamma \vdash_{\text{A}}^{\text{src}} \emptyset : \emptyset $$

S-TYP-BIND-SEQ

$$ \frac{\Gamma \vdash_{\text{A}}^{\text{src}} B_1 : D_1 \qquad \Gamma, A.I_1 : D_1 \vdash_{\text{A}}^{\text{src}} B_2 : D_2}{\Gamma \vdash_{\text{A}}^{\text{src}} B_1, B_2 : D_1 + D_2} $$
# D Canonical system – Complete rules

## D.1 Subtyping

Rules for both general and abstraction subtyping are shown, $<$: being either $<$: or $<>$:

### D.1.1 $\Gamma \stackrel{\text{can}}{\vdash} S <: S'$ – Signatures subtyping

C-SUB-SIG-FUNCTOR

$$ \frac{\Gamma, \bar{\alpha}' \vdash \mathcal{R}' <: \mathcal{R}[\bar{\alpha} \mapsto \bar{\tau}]}{\Gamma, \bar{\alpha}', (Y : \mathcal{R}') \vdash S[\bar{\alpha} \mapsto \bar{\tau}] <: S'} \quad Y \notin \Gamma \\ \Gamma \vdash \forall \bar{\alpha}. (Y : \mathcal{R}) \rightarrow S <: \forall \bar{\alpha}'. (Y : \mathcal{R}') \rightarrow S' $$

C-SUB-SIG-MATCH

$$ \frac{\Gamma, \bar{\alpha} \stackrel{\text{can}}{\vdash} \mathcal{R} <: \mathcal{R}'[\bar{\alpha}' \mapsto \bar{\tau}]}{\Gamma \stackrel{\text{can}}{\vdash} \exists \bar{\alpha}. \mathcal{R} <: \exists \bar{\alpha}'. \mathcal{R}'} $$

C-SUB-SIG-SIG

$$ \frac{\bar{\mathcal{D}}_0 \subseteq \bar{\mathcal{D}}}{\Gamma \vdash \mathcal{D} \end{array} \begin{array}{l} \bar{\mathcal{D}}' <: \bar{\mathcal{D}}' \\ \text{end} \end{array}} \Gamma \stackrel{\text{can}}{\vdash} \text{sig}_A \bar{\mathcal{D}} \text{ end} <: \text{sig}_A \bar{\mathcal{D}}' \text{ end} $$

C-SUB-EQ-SIG-SIG

$$ \frac{\Gamma \vdash \bar{\mathcal{D}} <: \bar{\mathcal{D}}'}{\Gamma \stackrel{\text{can}}{\vdash} \text{sig}_A \bar{\mathcal{D}} \text{ end} <: \text{sig}_A \bar{\mathcal{D}}' \text{ end}} $$

### D.1.2 $\Gamma \stackrel{\text{can}}{\vdash} \mathcal{D} <: \mathcal{D}'$ – Declarations subtyping

C-SUB-DECL-VAL

$$ \frac{\Gamma \stackrel{\text{can}}{\vdash} \tau <: \tau'}{\Gamma \stackrel{\text{can}}{\vdash} (\text{val } x : \tau) <: (\text{val } x : \tau')} $$

C-SUB-DECL-TYPE

$$ \frac{\Gamma \stackrel{\text{can}}{\vdash} \tau <: \tau'}{\Gamma \stackrel{\text{can}}{\vdash} (\text{type } t = \tau) <: (\text{type } t = \tau')} $$

C-SUB-DECL-MOD

$$ \frac{\Gamma \stackrel{\text{can}}{\vdash} \mathcal{R} <: \mathcal{R}'}{\Gamma \stackrel{\text{can}}{\vdash} (\mathit{module} X : \mathcal{R}) <: (\mathit{module} X : \mathcal{R}')} $$

C-SUB-DECL-MODTYPE

$$ \frac{\Gamma \stackrel{\text{can}}{\vdash} \mathcal{R} <: \mathcal{R}'}{\Gamma \stackrel{\text{can}}{\vdash} \mathcal{R}' <: \mathcal{R}} \qquad \Gamma \stackrel{\text{can}}{\vdash} \mathcal{R}' <: \mathcal{R} \\ \Gamma \stackrel{\text{can}}{\vdash} (\mathit{module} \ \mathit{type} \ T = \lambda \bar{\alpha}. \mathcal{R}) <: (\mathit{module} \ \mathit{type} \ T = \lambda \bar{\alpha}. \mathcal{R}') $$

## D.2 Typing

### D.2.1 $\Gamma \stackrel{\text{can}}{\vdash} Q.t : \tau$ – Type checking

C-TYP-TYPE-LOCALTYPE
$A.t : \mathit{type} t = \tau \in \Gamma$

$\Gamma \stackrel{\text{can}}{\vdash} A.t : \tau$

C-TYP-TYPE-PATHTYPE

$$ \frac{\Gamma \stackrel{\text{can}}{\vdash} P : \text{sig}_A \bar{\mathcal{D}} \text{ end}}{\Gamma \stackrel{\text{can}}{\vdash} P.t : \tau} \quad (\text{type } t = \tau) \in \bar{\mathcal{D}} $$
### D.2.2 $\Gamma \vdash_A^\text{can} D : \lambda \bar{\alpha}.D$ – Declaration typing

**C-TYP-DECL-VAL**

$$ \Gamma \vdash^\text{can} \tau : \tau' \qquad A.x \notin \Gamma $$

$$ \Gamma \vdash_A^\text{can} val x : \tau : val x : \tau' $$

**C-TYP-DECL-TYPE**

$$ \Gamma \vdash^\text{can} \tau : \tau' \qquad A.t \notin \Gamma $$

$$ \Gamma \vdash_A^\text{can} \text{type } t = \tau : \text{type } t = \tau' $$

**C-TYP-DECL-TYPEABS**

$$ \Gamma \vdash_A^\text{can} A.t \notin \Gamma $$

$$ \Gamma \vdash_A^\text{can} \text{type } t = A.t : \lambda \alpha. \text{type } t = \alpha $$

**C-TYP-DECL-MOD**

$$ \Gamma \vdash^\text{can} S : \lambda \bar{\alpha}.\mathcal{R} \qquad A.X \notin \Gamma $$

$$ \Gamma \vdash_A^\text{can} (\mathcal{M} \mathcal{X} : S) : \lambda \bar{\alpha}. (\mathcal{M} \mathcal{X} : \mathcal{R}) $$

**C-TYP-DECL-MODTYPE**

$$ \Gamma \vdash^\text{can} S : \lambda \bar{\alpha}.\mathcal{R} \qquad A.T \notin \Gamma $$

$$ \Gamma \vdash_A^\text{can} (\mathcal{M} \mathcal{D} \mathcal{T} : S) : (\mathcal{M} \mathcal{D} \mathcal{T} : \lambda \bar{\alpha}.\mathcal{R}) $$

**C-TYP-DECL-EMPTY**

$$ \Gamma \vdash_A^\text{can} \emptyset : \emptyset $$

**C-TYP-DECL-SEQ**

$$ \Gamma \vdash_A^\text{can} D_1 : \lambda \bar{\alpha}_1.D_1 \qquad \Gamma, \bar{\alpha}_1, A.I_1 : D_1 \vdash_A^\text{can} \bar{D} : \lambda \bar{\alpha}.\bar{D} $$

$$ \Gamma \vdash_A^\text{can} (D_1, \bar{D}) : \lambda \bar{\alpha}_1 \bar{\alpha}. (D_1, \bar{D}) $$

### D.2.3 $\Gamma \vdash^\text{can} S : \lambda \bar{\alpha}.\mathcal{R}$ – Signature typing

**C-TYP-SIG-SIG**

$$ \Gamma \vdash^\text{can}_A \bar{D} : \lambda \bar{\alpha}.\bar{D} \qquad A \notin \Gamma $$

$$ \Gamma \vdash^\text{can}_A \mathcal{S} \mathcal{I}_A \bar{D} \text{ end} : \lambda \bar{\alpha}.\mathcal{S} \mathcal{I}_A \bar{D} \text{ end} $$

**C-CF-MODTYPE**

$$ \Gamma \vdash^\text{can}_P \mathcal{S} \mathcal{I}_A \bar{D} \text{ end} \qquad \mathbf{module type} \ T = \lambda \bar{\alpha}.\mathcal{R} \in \bar{D} $$

$$ \Gamma \vdash^\text{can}_A A.T : \lambda \bar{\alpha}.\mathcal{R} $$

$$ \text{C-TYP-SIG-LOCALMODTYPE} \qquad (A.T : \mathbf{module type} \ T = \lambda \bar{\alpha}.\mathcal{R}) \in \Gamma $$

$$ \Gamma \vdash^\text{can}_A A.T : \lambda \bar{\alpha}.\mathcal{R} $$

**C-TYP-SIG-FUNCTOR**

$$ \Gamma \vdash^\text{can}_S S_a : \lambda \bar{\alpha}.\mathcal{R}_a \qquad \Gamma, \bar{\alpha}, Y : \mathcal{R}_a \vdash^\text{can}_S S : \lambda \bar{\beta}.\mathcal{R} \qquad Y \notin \Gamma $$

$$ \Gamma \vdash^\text{can}_Y (Y : S_a) \to S : \forall \bar{\alpha}. (Y : \mathcal{R}_a) \to \exists \bar{\beta}.\mathcal{R} $$

### D.2.4 $\Gamma \vdash^\text{can} M : S$ – Module typing
C-TYP-MOD-FCTARG

$$ \frac{(Y : \mathcal{R}) \in \Gamma}{\Gamma \vdash Y : \mathcal{R}} $$

C-TYP-MOD-LOCAL

$$ \frac{(A.X : \mathcal{R}) \in \Gamma}{\Gamma \vdash A.X : \mathcal{R}} $$

C-TYP-STRUCT

$$ \frac{\Gamma \vdash_A B : \exists \bar{\alpha}. \bar{D} \quad A \notin \Gamma}{\Gamma \vdash \mathit{struct}_A B \ \mathit{end} : \exists \bar{\alpha}. \mathit{sig}_A \bar{D} \ \mathit{end}} $$

C-TYP-MOD-SEALING

$$ \frac{\Gamma \vdash S : \lambda \bar{\alpha}. \mathcal{R} \qquad \Gamma \vdash P : \mathcal{R}' \qquad \Gamma \vdash \mathcal{R}' < : \mathcal{R}[\bar{\alpha} \mapsto \bar{\tau}]}{\Gamma \vdash (P : S) : \exists \bar{\alpha}. \mathcal{R}} $$

C-TYP-MOD-FUNCTOR

$$ \frac{\Gamma \vdash S : \lambda \bar{\alpha}. \mathcal{R} \qquad \Gamma, \bar{\alpha}, (Y : \mathcal{R}) \vdash M : S}{\Gamma \vdash (Y : S) \to M : \forall \bar{\alpha}. (Y : \mathcal{R}) \to S} $$

C-TYP-MOD-APP

$$ \frac{\Gamma \vdash P : \forall \bar{\alpha}. (Y : \mathcal{R}) \to S \qquad \Gamma \vdash P' : \mathcal{R}' \qquad \Gamma \vdash \mathcal{R}' < : \mathcal{R}[\bar{\alpha} \mapsto \bar{\tau}]}{\Gamma \vdash P(P') : S[\bar{\alpha} \mapsto \bar{\tau}]} $$

C-TYP-MOD-PROJ

$$ \frac{\Gamma \vdash M : \exists \bar{\alpha}. \mathit{sig}_A \bar{D}_1, \mathit{module} X : \mathcal{R}, \bar{D}_2 \ \mathit{end}}{\Gamma \vdash M.X : \exists \bar{\alpha}. \mathcal{R}} $$

### D.2.5 $\Gamma \vdash_A B : \exists \bar{\alpha}. \mathcal{D}$ – Bindings typing

C-TYP-DECL-LET

$$ \frac{\Gamma \vdash e : \tau \qquad \Gamma \vdash \tau : \tau' \qquad A.x \notin \Gamma}{\Gamma \vdash_A (\mathit{let} \ x = e) : (\mathit{val} \ x : \tau')} $$

C-TYP-DECL-TYPE

$$ \frac{\Gamma \vdash \tau : \tau' \qquad A.t \notin \Gamma}{\Gamma \vdash_A (\mathit{type} \ t = \tau) : (\mathit{type} \ t = \tau')} $$

C-TYP-DECL-MOD

$$ \frac{\Gamma \vdash M : \exists \bar{\alpha}. \mathcal{R} \qquad A.X \notin \Gamma}{\Gamma \vdash_A (\mathit{module} \ X = M) : (\exists \bar{\alpha}. \mathit{module} \ X : \mathcal{R})} $$

C-TYP-DECL-MODTYPE

$$ \frac{\Gamma \vdash S : \lambda \bar{\alpha}. \mathcal{R} \qquad A.T \notin \Gamma}{\Gamma \vdash_A (\mathit{module} \ \mathit{type} \ T = S) : (\mathit{module} \ \mathit{type} \ T = \lambda \bar{\alpha}. \mathcal{R})} $$

C-TYP-DECL-EMPTY

$$ \Gamma \vdash_A \emptyset : \emptyset $$

C-TYP-DECL-SEQ

$$ \frac{\Gamma \vdash_A B_1 : \exists \bar{\alpha}_1. \mathcal{D}_1 \qquad \Gamma, \bar{\alpha}_1, A.I_1 : \mathcal{D}_1 \vdash_A \bar{B} : \exists \bar{\alpha}. \bar{D}}{\Gamma \vdash_A B_1, \bar{B} : \exists \bar{\alpha}_1 \bar{\alpha}. \bar{D}_1, \bar{D}} $$

## D.3 Anchoring
### D.3.1 $\Gamma \vdash \tau \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \tau' - \text{Type anchoring}$

$$
\begin{array}{c}
\text{C-ACH-TYPE-ANCHOR} \\
\frac{\Gamma \leftrightarrow \Gamma_s : \theta_\Gamma \qquad \theta_\Gamma(\alpha) = Q.t}{\Gamma \vdash \alpha \leftrightarrow \Gamma_s; \theta_\Gamma \vdash Q.t}
\end{array}
$$

$$
\begin{array}{c}
\text{C-ACH-DECL-TYPE} \\
\frac{\Gamma \vdash \tau \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \tau' : \emptyset}{\Gamma \vdash_A \text{ type } t = \tau \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \text{ type } t = \tau' : \emptyset}
\end{array}
$$

### D.3.2 $\Gamma \vdash_A^{anc} D \leftrightarrow \Gamma_s; \theta_\Gamma \vdash D : \theta$ - Declaration anchoring

$$
\begin{array}{c}
\text{C-ACH-DECL-VAL} \\
\frac{\Gamma \vdash \tau \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \tau' : \emptyset}{\Gamma \vdash_A^{anc} \text{ val } x : \tau \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \text{ val } x : \tau' : \emptyset}
\end{array}
$$

$$
\begin{array}{c}
\text{C-ACH-DECL-ANCHORPOINT} \\
\frac{\Gamma \leftrightarrow \Gamma_s : \theta_\Gamma \qquad \alpha \notin \text{dom}(\theta_\Gamma)}{\Gamma \vdash_A^{anc} \text{ type } t = \alpha \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \text{ type } t = A.t : (\alpha \mapsto t)}
\end{array}
$$

$$
\begin{array}{c}
\text{C-ACH-DECL-TYPE} \\
\frac{\Gamma \vdash \tau \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \tau' : \emptyset}{\Gamma \vdash_A^{anc} \text{ type } t = \tau \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \text{ type } t = \tau' : \emptyset}
\end{array}
$$

$$
\begin{array}{c}
\text{C-ACH-DECL-MOD} \\
\frac{\Gamma \vdash \mathcal{R} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash S : \theta}{\Gamma \vdash_A^{anc} \text{ module } X : \mathcal{R} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \text{ module } X : S : X.\theta}
\end{array}
$$

$$
\begin{array}{c}
\text{C-ACH-DECL-SIG} \\
\frac{\Gamma, \bar{\alpha} \vdash \mathcal{R} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash S : \theta}{\Gamma \vdash_A^{anc} \text{ module } T : \lambda \bar{\alpha}. \mathcal{R} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \text{ module } T : S : \emptyset}
\end{array}
$$

$$
\begin{array}{c}
\text{C-ACH-DECL-SEQ} \\
\frac{\Gamma \vdash_D^{anc} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash D : \theta}{\Gamma \vdash_D^{anc} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash D, \bar{D} : \theta_\Gamma \uplus \theta'}
\end{array}
$$

### D.3.3 $\Gamma \vdash S : \lambda \bar{\alpha}. \mathcal{R}$ - Signature anchoring

$$
\begin{array}{c}
\text{C-ACH-SIG-FUNCTOR} \\
\frac{\Gamma, \bar{\alpha} \vdash \mathcal{R} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash S_a : \theta_a}{\text{dom}(\theta_a) = \bar{\alpha} \qquad \Gamma, \bar{\alpha}, Y : \mathcal{R} \vdash S \leftrightarrow (\Gamma_s, Y : S_a); (\theta_\Gamma \uplus Y.\theta) \vdash S : \theta} \\
\frac{\Gamma \vdash \forall \bar{\alpha}. (Y : \mathcal{R}) \to S \leftrightarrow \Gamma_s; \theta_\Gamma \vdash (Y : S_a) \to S : \emptyset}{\Gamma \vdash \forall \bar{\alpha}. (Y : \mathcal{R}) \to S \leftrightarrow \Gamma_s; \theta_\Gamma \vdash (Y : S_a) \to S : \emptyset}
\end{array}
$$

$$
\begin{array}{c}
\text{C-ACH-SIG-SIG} \\
\frac{\Gamma \vdash_A^{anc} \bar{D} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \bar{D} : \theta}{\Gamma \vdash^{anc} \text{ sig}_A \bar{D} \text{ end} \leftrightarrow \Gamma_s; \theta_\Gamma \vdash \text{ sig}_A \bar{D} \text{ end} : \theta}
\end{array}
$$
### D.3.4 $\Gamma \hookrightarrow \Gamma_s : \theta_\Gamma$ - Environment anchoring

C-ACH-ENV-EMPTY

$\emptyset \hookrightarrow \emptyset : \emptyset$

C-ACH-ENV-FCTARG

$$ \frac{\Gamma \hookrightarrow \Gamma_s : \theta_\Gamma \quad \Gamma, \bar{\alpha} \vdash_R \mathcal{R} \hookrightarrow \Gamma_s; \theta_\Gamma \vdash S : \theta \quad \text{dom}(\theta) = \bar{\alpha}}{\Gamma, \bar{\alpha}, Y : \mathcal{R} \hookrightarrow (\Gamma_s, Y : S) : \theta_\Gamma \uplus Y.\theta} $$

C-ACH-ENV-DECL

$$ \frac{\Gamma \hookrightarrow \Gamma_s : \theta_\Gamma \quad \Gamma, \bar{\alpha} \vdash_A^\text{anc} \mathcal{D} \hookrightarrow \Gamma_s; \theta_\Gamma \vdash D : \theta \quad \text{dom}(\theta) = \bar{\alpha}}{\Gamma, \bar{\alpha}, A.I : \mathcal{D} \hookrightarrow (\Gamma_s, A.I : D) : \theta_\Gamma \uplus A.\theta} $$

### D.3.5 $\Gamma \vdash^\text{anc} M : S$ - Anchorable typing

C-TYPA-MOD-PROJ

$$ \frac{\Gamma \vdash^\text{anc} M : \exists \bar{\alpha}. \text{sig}_A \bar{\mathcal{D}}_1, \text{module } X : \mathcal{R}, \bar{\mathcal{D}}_2 \text{ end} \quad \Gamma \vdash^\text{anc} \exists \bar{\alpha}. \mathcal{R} \hookrightarrow \Gamma_s; \theta_\Gamma \vdash S : \theta}{\Gamma \vdash^\text{anc} M.X : \exists \bar{\alpha}. \mathcal{R}} $$
# E F<sup>ω</sup>- Complete rules

## E.1 Γ : **wf** – Environment checking

$$ \begin{array}{c} \therefore : \mathit{wf} \\ \frac{\Gamma : \mathit{wf} \qquad \alpha \notin \Gamma}{\Gamma, \alpha : \kappa : \mathit{wf}} \qquad \frac{\Gamma \vdash \tau : \star \qquad x \notin \Gamma}{\Gamma, (x : \tau) : \mathit{wf}} \end{array} $$

## E.2 Γ ⊢ τ : κ – Type checking

$$ \frac{\Gamma \vdash \tau_1 : \star \qquad \Gamma \vdash \tau_2 : \star}{\Gamma \vdash \tau_1 \rightarrow \tau_2 : \star} \qquad \frac{\Gamma \vdash \tau : \star \qquad \Gamma : \mathit{wf}}{\Gamma \vdash \{\overline{l}_1 : \tau\} : \star} \qquad \frac{\Gamma : \mathit{wf}}{\Gamma \vdash \alpha : \Gamma(\alpha)} \qquad \frac{\Gamma, \alpha : \kappa \vdash \tau : \star}{\Gamma \vdash \forall \alpha : \kappa.\tau : \star} $$

$$ \frac{\Gamma, \alpha : \kappa \vdash \tau : \star}{\Gamma \vdash \exists \alpha : \kappa.\tau : \star} \qquad \frac{\Gamma, \alpha : \kappa \vdash \tau : \kappa'}{\Gamma \vdash \lambda \alpha : \kappa.\tau : \kappa \rightarrow \kappa'} \qquad \frac{\Gamma \vdash \tau_1 : \kappa' \rightarrow \kappa}{\Gamma \vdash \tau_1 \tau_2 : \kappa} $$

## E.3 Γ ⊢ e : τ – Term typing

$$ \frac{\Gamma : \mathit{wf}}{\Gamma \vdash x : \Gamma(x)} \qquad \frac{\Gamma, x : \tau \vdash e : \tau'}{\Gamma \vdash \lambda x : \tau. e : \tau \rightarrow \tau'} \qquad \frac{\Gamma \vdash e_1 : \tau' \rightarrow \tau}{\Gamma \vdash e_1 e_2 : \tau'} $$

$$ \frac{\Gamma \vdash e : \tau}{\Gamma \vdash \{\overline{l} = e\} : \{\overline{l} : \tau\}} \qquad \frac{\Gamma \vdash e : \{l : \tau, \overline{l'} : \tau'\}}{\Gamma \vdash e.l : \tau} \qquad \frac{\Gamma, \alpha : \kappa \vdash e : \tau}{\Gamma \vdash \Lambda(\alpha : \kappa).e : \forall(\alpha : \kappa).\tau} $$

$$ \frac{\Gamma \vdash e : \forall \alpha : \kappa.\tau'}{\Gamma \vdash e : \tau : \kappa} \qquad \frac{\Gamma \vdash \tau : \kappa}{\Gamma \vdash \mathit{pack}(\tau, e) \text{ as } \exists \alpha : \kappa.\tau' : \star} $$

$$ \frac{\Gamma \vdash e_1 : \exists \alpha : \kappa.\tau'}{\Gamma \vdash \mathit{unpack}(\alpha, x) = e_1 \text{ in } e_2 : \tau} \qquad \frac{\Gamma, \alpha : \kappa, x : \tau' \vdash e_2 : \tau}{\Gamma \vdash \tau : \star} $$

# F Elaborated system – Complete rules

## F.1 Subtyping

### F.1.1 Δ ⊢ S <: S' ↪ → Π <: Π' ⇒ f – Signature subtyping
E-SUB-SIG-FUNCTOR

$$ \Delta, \bar{\alpha}' \overset{\text{elab}}{\vdash} \mathcal{R}'_a <: \mathcal{R}_a[\bar{\alpha} \mapsto \bar{\tau}] \rightsquigarrow \Sigma'_a <: \Sigma_a[\bar{\alpha} \mapsto \bar{\tau}] \Rightarrow f_a $$

$$ \Delta, \bar{\alpha}', (Y : (\mathcal{R}'_a, \Sigma'_a)) \overset{\text{elab}}{\vdash} \mathcal{S}[\bar{\alpha} \mapsto \bar{\tau}] <: \mathcal{S}' \rightsquigarrow \Pi[\bar{\alpha} \mapsto \bar{\tau}] <: \Pi' \Rightarrow f \quad Y \notin \Delta $$

$$ \Delta \vdash \forall \bar{\alpha}. (Y : \mathcal{R}_a) \to \mathcal{S} <: \forall \bar{\alpha}'. (Y : \mathcal{R}'_a) \to \mathcal{S}' \rightsquigarrow \forall \bar{\alpha}. \Sigma_a \to \Pi <: \forall \bar{\alpha}'. \Sigma'_a \to \Pi' \\ [\lambda (g : (\forall \bar{\alpha}. \Sigma_a \to \Pi)). \Lambda \bar{\alpha}'. \lambda (x : \Sigma'_a) . f (g \bar{\tau} (f_a x))] $$

E-SUB-SIG-SIG

$$ \overline{\mathcal{D}}_0 \subseteq \overline{\mathcal{D}} \qquad \Delta \vdash_A \overline{\mathcal{D}}_0 <: \overline{\mathcal{D}}' \rightsquigarrow \overline{\zeta}_0 <: \overline{\zeta} \Rightarrow \overline{f} $$

$$ \Delta \vdash \mathit{sig}_A \overline{\mathcal{D}} \mathit{end} <: \mathit{sig}_A \overline{\mathcal{D}}' \mathit{end} \rightsquigarrow \{\overline{\ell_I : \zeta}\} <: \{\overline{\ell_I : \zeta'}\} \Rightarrow \lambda x. \{\overline{\ell_{I_0} : (f \zeta)}\} $$

E-SUBEQ-SIG-SIG

$$ \Delta \vdash_A \overline{\mathcal{D}} <: \overline{\mathcal{D}}' \rightsquigarrow \overline{\zeta} <: \overline{\zeta'} \Rightarrow \overline{f} $$

$$ \Delta \vdash \mathit{sig}_A \overline{\mathcal{D}} \mathit{end} <: \mathit{sig}_A \overline{\mathcal{D}}' \mathit{end} \rightsquigarrow \{\overline{\ell_I : \zeta}\} <: \{\overline{\ell_I : \zeta'}\} \Rightarrow \lambda x. \{\overline{\ell_I : (f \zeta)}\} $$

### F.1.2 $\Delta \vdash_A^{\text{elab}} \mathcal{D} <: \mathcal{D}' \rightsquigarrow \zeta <: \zeta' \Rightarrow f$ - Declaration subtyping

E-SUB-VAL

$$ \Delta \vdash \tau <: \tau' \uparrow f $$

$$ \Delta \vdash_A (\mathit{val} x : \tau) <: (\mathit{val} x : \tau') \rightsquigarrow [[\tau]] <: [[\tau')] \Rightarrow \lambda x. [[f(x.\mathit{val})]] $$

E-SUB-TYPE

$$ \Delta \vdash \tau <: \tau' \uparrow f $$

$$ \Delta \vdash_A^{\text{elab}} (\mathit{type} t = \tau) <: (\mathit{type} t = \tau') \rightsquigarrow [[\tau : \kappa]] <: [[\tau' : \kappa]] \Rightarrow \lambda x. [[\tau' : \kappa]] $$

E-SUB-MOD

$$ \Delta \vdash \mathcal{R} <: \mathcal{R}' \rightsquigarrow \Sigma <: \Sigma' \Rightarrow f $$

$$ \Delta \vdash_A^{\text{elab}} (\mathit{module} X : \mathcal{R}) <: (\mathit{module} X : \mathcal{R}') \rightsquigarrow [[\Sigma]] <: [[\Sigma']]] \Rightarrow \lambda x. [[f(x.\mathit{mod})]] $$

E-SUB-MODTYPE

$$ \Delta, \bar{\alpha} \vdash \mathcal{R} <: \mathcal{R}' \rightsquigarrow \Sigma <: \Sigma' \Rightarrow f $$

$$ \Delta, \bar{\alpha} \vdash \mathcal{R}' <: \mathcal{R} \rightsquigarrow \Sigma' <: \Sigma \Rightarrow f' $$

$$ \Delta \vdash_A^{\text{elab}} (\mathit{module} \ type \ T = \lambda \bar{\alpha}. \mathcal{R}) <: (\mathit{module} \ type \ T = \lambda \bar{\alpha}. \mathcal{R}') \rightsquigarrow [[\lambda \bar{\alpha}. \Sigma]] <: [[\lambda \bar{\alpha}. \Sigma']]] \\ \Rightarrow \lambda x. [[\lambda \bar{\alpha}. \Sigma']]] $$

## F.2 Typing

### F.2.1 $\Delta \vdash Q.t : \tau$ - Type checking
$$
\begin{array}{c}
\text{E-TYP-TYPE-LOCALTYPE} \\
\Delta \vdash_{\text{elab}} A.t : \tau
\end{array}
$$

$$
\begin{array}{c}
\text{E-TYP-TYPE-PATHTYPE} \\
\Delta \vdash_{\text{elab}} P : \text{sig}_A \bar{D} \text{ end} \rightsquigarrow_- : \Sigma \quad (\text{type } t = \tau) \in \bar{D} \quad \Sigma.\ell_t : \langle\langle \tau \rangle\rangle \\
\Delta \vdash P.t : \tau
\end{array}
$$

F.2.2 $\Delta \vdash_A^{\text{elab}} D : \lambda\bar{\alpha}.D \rightsquigarrow \lambda\bar{\alpha}.\zeta$ - Declaration typing

$$
\begin{array}{c}
\text{E-TYP-DECL-VAL} \\
\Delta \vdash^{\text{elab}} \tau : \tau' \qquad A.x \notin \Delta \\
\Delta \vdash_A^{\text{elab}} val : \tau : val : \tau' \rightsquigarrow^{\text{elab}} val : \tau'
\end{array}
$$

$$
\begin{array}{c}
\text{E-TYP-DECL-TYPE} \\
\Delta \vdash^{\text{elab}} \tau : \tau' \qquad A.t \notin \Delta \\
\Delta \vdash_A^{\text{elab}} \text{type } t = \tau : \text{type } t = \tau' \rightsquigarrow^{\text{elab}} \text{type } t = \tau'
\end{array}
$$

$$
\begin{array}{c}
\text{E-TYP-DECL-TYPEABS} \\
\Delta \vdash_A^{\text{elab}} \text{type } t = A.t : \lambda\alpha. \text{type } t = \alpha \rightsquigarrow^{\lambda\alpha.} \lambda\alpha. \text{type } t = \alpha
\end{array}
$$

$$
\begin{array}{c}
\text{E-TYP-DECL-MOD} \\
\Delta \vdash_S^{\text{elab}} : \lambda\bar{\alpha}.\mathcal{R} \rightsquigarrow \lambda\bar{\alpha}.\Sigma \qquad A.X \notin \Delta \\
\Delta \vdash_A^{\text{elab}} (\mathit{module} X : S) : \lambda\bar{\alpha}. (\mathit{module} X : \mathcal{R}) \rightsquigarrow \lambda\bar{\alpha}. \mathit{module} X : \Sigma
\end{array}
$$

$$
\begin{array}{c}
\text{E-TYP-DECL-MODTYPE} \\
\Delta \vdash_S^{\text{elab}} : \lambda\bar{\alpha}.\mathcal{R} \rightsquigarrow \lambda\bar{\alpha}.\Sigma \qquad A.T \notin \Delta \\
\Delta \vdash_A^{\text{elab}} (\mathit{module type } T = S) : (\mathit{module type } T = \lambda\bar{\alpha}.\mathcal{R}) \rightsquigarrow (\mathit{module type } T = \lambda\bar{\alpha}.\Sigma)
\end{array}
$$

$$
\begin{array}{c}
\text{E-TYP-DECL-EMPTY} \\
\Delta \vdash_A^{\text{elab}} \emptyset : \emptyset \rightsquigarrow \emptyset
\end{array}
$$

$$
\begin{array}{c}
\text{E-TYP-DECL-SEQ} \\
\Delta \vdash_A^{\text{elab}} D_1 : \lambda \bar{\alpha}_1 . \mathcal{D}_1 \rightsquigarrow \lambda \bar{\alpha}_1 . \zeta_1 \qquad \Delta, \bar{\alpha}_1, A.I_1 : (\mathcal{D}_1, \zeta_1) \vdash_A^{\text{elab}} \bar{D} : \lambda \bar{\alpha} . \bar{D} \rightsquigarrow \lambda \bar{\alpha} . \bar{\zeta} \\
\Delta \vdash_A^{\text{elab}} (\mathcal{D}_1, \bar{D}) : \lambda \bar{\alpha}_1 \bar{\alpha} . (\mathcal{D}_1, \bar{D}) \rightsquigarrow \lambda \bar{\alpha}_1 \bar{\alpha} . (\zeta_1, \bar{\zeta})
\end{array}
$$

F.2.3 $\Delta \vdash_S^{\text{elab}} : \lambda\bar{\alpha}.\mathcal{R} \rightsquigarrow \lambda\bar{\alpha}.\Sigma$ - Signature typing
E-TYP-SIG-SIG

$$ \frac{\Delta \vdash_A \bar{D} : \lambda\bar{\alpha}.\bar{D} \rightsquigarrow \lambda\bar{\alpha}.\bar{\zeta} \quad A \notin \Delta}{\Delta \vdash \mathrm{sig}_A \bar{D} \mathrm{end} : \lambda\bar{\alpha}.\mathrm{sig}_A \bar{D} \mathrm{end} \rightsquigarrow \lambda\bar{\alpha}.\{\zeta\}} $$

E-CF-MODTYPE

$$ \frac{\Delta \vdash_P \mathit{sig}_A \bar{D} \mathit{end} \rightsquigarrow \mathit{\_} : \Sigma'}{\Delta \vdash A.T : \lambda\bar{\alpha}.\mathcal{R} \rightsquigarrow \lambda\bar{\alpha}.\Sigma} \qquad \text{module type } T = \lambda\bar{\alpha}.\mathcal{R} \in \bar{D} \qquad \Sigma' . \ell_T : \langle\!\langle \lambda\bar{\alpha} . \Sigma \rangle\!\rangle $$

E-TYP-SIG-LOCALMODTYPE

$$ \frac{A.I : (\mathit{module type} \ T = \lambda\bar{\alpha}.\mathcal{R}, \mathit{module type} \ T = \lambda\bar{\alpha}.\Sigma) \in \Delta}{\Delta \vdash A.T : \lambda\bar{\alpha}.\mathcal{R} \rightsquigarrow \lambda\bar{\alpha}.\Sigma} $$

E-TYP-SIG-FUNCTOR

$$ \frac{\Delta \vdash S_a : \lambda\bar{\alpha}.\mathcal{R}_a \rightsquigarrow \lambda\bar{\alpha}.\Sigma_a}{\Delta, \bar{\alpha}, Y : (\mathcal{R}_a, \Sigma_a) \vdash S : \lambda\bar{\beta}.\mathcal{R} \rightsquigarrow \lambda\bar{\beta}.\Sigma} \quad Y \notin \Delta \\ \Delta \vdash (Y : S_a) \rightarrow S : \forall\bar{\alpha}. (Y : \mathcal{R}_a) \rightarrow \exists\bar{\beta}.\mathcal{R} \rightsquigarrow \forall\bar{\alpha}.\Sigma_a \rightarrow \exists\bar{\beta}.\Sigma $$

**F.2.4** $\Delta \vdash_M S \rightsquigarrow e : \Pi$ - Module typing
E-TYP-MOD-FCTARG

$$ \frac{Y : (\mathcal{R}, \Sigma) \in \Delta}{\Delta \vdash_{\text{elab}} Y : \mathcal{R} \rightsquigarrow Y : \Sigma} $$

E-TYP-MOD-LOCAL

$$ \frac{A.X : (\mathcal{R}, \Sigma) \in \Delta}{\Delta \vdash_{\text{elab}} A.X : \mathcal{R} \rightsquigarrow A.X : \Sigma} $$

E-TYP-STRUCT

$$ \frac{\Delta \vdash_{\text{elab}} B : \exists \bar{\alpha}. \bar{D} \rightsquigarrow e : \exists \bar{\alpha}. \{\bar{\zeta}\} \quad A \notin \Delta}{\Delta \vdash \text{struct}_A B \text{ end} : \exists \bar{\alpha}. \text{sig}_A \bar{D} \text{ end} \rightsquigarrow e : \exists \bar{\alpha}. \{\bar{\zeta}\}} $$

E-TYP-MOD-SEALING

$$ \frac{\Delta \vdash_{\text{elab}} S : \lambda \bar{\alpha}. \mathcal{R} \rightsquigarrow \lambda \bar{\alpha}. \Sigma}{\Delta \vdash_{\text{elab}} P : \mathcal{R}' \rightsquigarrow e : \Sigma'} \qquad \frac{\Delta \vdash_{\text{elab}} \mathcal{R}' < : \mathcal{R}[\bar{\alpha} \mapsto \bar{\tau}] \rightsquigarrow \Sigma' < : \Sigma[\bar{\alpha} \mapsto \bar{\tau}] \Rightarrow f}{\Delta \vdash_{\text{elab}} (P : S) : \exists \bar{\alpha}. \mathcal{R} \rightsquigarrow \text{pack}(\bar{\tau}, (f e)) : \lambda \bar{\alpha}. \Sigma} $$

E-TYP-MOD-FUNCTOR

$$ \frac{\Delta \vdash_{\text{elab}} S : \lambda \bar{\alpha}. \mathcal{R} \rightsquigarrow \lambda \bar{\alpha}. \Sigma}{\Delta \vdash_{\text{elab}} (Y : S) \to M : \forall \bar{\alpha}. (Y : \mathcal{R}) \to S \rightsquigarrow \forall \bar{\alpha}. \lambda(Y : \mathcal{R}).e : \forall \bar{\alpha}. \Sigma \to \Pi} $$

E-TYP-MOD-APP

$$ \frac{\Delta \vdash_{\text{elab}} P : \forall \bar{\alpha}. (Y : \mathcal{R}) \to S \rightsquigarrow e_P : \forall \bar{\alpha}. \Sigma \to S}{\Delta \vdash_{\text{elab}} P' : \mathcal{R}' \rightsquigarrow e : \Sigma'} \qquad \frac{\Delta \vdash_{\text{elab}} \mathcal{R}' < : \mathcal{R}[\bar{\alpha} \mapsto \bar{\tau}] \rightsquigarrow \Sigma' < : \Sigma[\bar{\alpha} \mapsto \bar{\tau}] \Rightarrow f}{\Delta \vdash_{\text{elab}} P(P') : \mathcal{R}[\bar{\alpha} \mapsto \bar{\tau}] \rightsquigarrow e_P \bar{\tau} (f e) : \Pi[\bar{\alpha} \mapsto \bar{\tau}]} $$

E-TYP-MOD-PROJ

$$ \frac{\Delta \vdash_{\text{elab}} M : \exists \bar{\alpha}. \text{sig}_A \bar{D}_1, \text{module } X : \mathcal{R}, \bar{D}_2 \text{ end} \rightsquigarrow e : \{\bar{\zeta}_1, \ell_X : \Sigma, \bar{\zeta}_2\}}{\Delta \vdash_{\text{elab}} M.X : \exists \bar{\alpha}. \mathcal{R} \rightsquigarrow \text{unpack}(\bar{\alpha}, y) = e \text{ in } \text{pack}(\bar{\alpha}, e.\ell_X) : \exists \bar{\alpha}. \Sigma} $$

F.2.5 $\Delta \vdash_{\text{elab}} B : \exists \bar{\alpha}. \bar{D} \rightsquigarrow e : \exists \bar{\alpha}. \{\bar{\ell}_I : \bar{\zeta}\} - \text{Bindings typing}$
E-TYP-DECL-LET

$$
\frac{\Delta \vdash^{\text{elab}} e : \tau \leadsto e' : \tau'}{\Delta \vdash_A (\text{let } x = e) : (\text{val } x : \tau') \leadsto \{\ell_x = e'\} : (\text{val } x : \tau')}
$$

E-TYP-DECL-TYPE

$$
\frac{\Delta \vdash^{\text{elab}} \tau : \tau' \quad A.t \notin \Delta}{\Delta \vdash_A (\text{type } t = \tau) : (\text{type } t = \tau') \leadsto \{\ell_t = \langle\langle \tau' \rangle\rangle\} : (\text{type } t = \tau')}
$$

E-TYP-DECL-MOD

$$
\frac{\Delta \vdash^\text{elab} M : \exists \bar{\alpha}. \mathcal{R} \leadsto e : \exists \bar{\alpha}. \Sigma \quad A.X \notin \Delta}{\Delta \vdash_A^\text{elab} (\text{module } X = M) : (\exists \bar{\alpha}. \text{module } X : \mathcal{R}) \leadsto \text{unpack}(\bar{\alpha}, y) = e \text{ in } \text{pack}(\bar{\alpha}, \{\ell_X = y\}) : \exists \bar{\alpha}. \text{module } X : \Sigma}
$$

E-TYP-DECL-MODTYPE

$$
\frac{\Delta \vdash^\text{elab} S : \lambda\bar{\alpha}.\mathcal{R} \leadsto \lambda\bar{\alpha}.\Sigma \quad A.T \notin \Delta}{\Delta \vdash_A^\text{elab} (\text{module type } T = S) : (\text{module type } T = \lambda\bar{\alpha}.\mathcal{R}) \leadsto \{\ell_T = \langle\langle \lambda\bar{\alpha}.\mathcal{R} \rangle\rangle\} : (\text{module type } T = \lambda\bar{\alpha}.\mathcal{R})}
$$

E-TYP-DECL-SEQ

$$
\frac{\Delta \vdash_A^\text{elab} B_1 : \exists \bar{\alpha}_1. \mathcal{D}_1 \leadsto e_1 : \exists \bar{\alpha}_1. \{\zeta_1\} \quad \Delta, \bar{\alpha}_1, A.I_1 : (\mathcal{D}_1, \zeta_1) \vdash_A^\text{elab} \bar{B} : \exists \bar{\alpha}. \bar{\mathcal{D}} \leadsto e : \exists \bar{\alpha}. \{\bar{\zeta}\}}{\Delta \vdash_A^\text{elab} B_1, \bar{B} : \exists \bar{\alpha}_1 \bar{\alpha}. \bar{\mathcal{D}}_1, \bar{\mathcal{D}} \leadsto \begin{array}{@{}l@{}} \text{unpack}(\bar{\alpha}_1, x_1) = e_1 \text{ in} \qquad : \exists \bar{\alpha}_1 \bar{\alpha}. \{\zeta_1, \bar{\zeta}\} \\ \text{unpack}(\bar{\alpha}, x) = (\text{let } A.I_1 = x_1. \ell_{I_1} \text{ in } e) \text{ in} \\ \text{pack}(\bar{\alpha}_1 \bar{\alpha}, \{\ell_I = x_1. \ell_I, \bar{\ell}_I = x. \ell_I\}) \end{array}}
$$
# Analyse de dépendance vérifiée pour un langage synchrone
à flot de données

Timothy Bourke¹,², Basile Pesin¹,², Marc Pouzet²,¹

¹ Inria Paris, France

² Département d'informatique de l'École normale supérieure, CNRS, PSL University, Paris, France

## Résumé

Vélus est une formalisation d'un langage synchrone à flots de données et de sa compilation dans l'assistant de preuve Coq. Il inclut une définition de la sémantique dynamique du langage, un compilateur produisant du code impératif, et une preuve de bout en bout que le compilateur préserve la sémantique des programmes.

Dans cet article, on spécifie dans Vélus la sémantique de deux structures d'activation présentes dans les compilateurs modernes : switch et déclarations locales. Ces nouvelles constructions nécessitent une adaptation de l'analyse statique de dépendance de Vélus, qui produit un graphe acyclique comme témoin de la bonne formation d'un programme. On utilise ce témoin pour construire un schéma d'induction propre aux programmes bien formés. Ce schéma permet de démontrer le déterminisme du modèle sémantique dans Coq.

## 1 Introduction

Le projet Vélus [3, 4, 5] formalise un langage synchrone à flot de données dans l'assistant de preuve Coq [11]. Ce langage est un sous-ensemble du langage industriel Scade 6 [9], qui est utilisé pour la spécification de systèmes de contrôle embarqués critiques. Scade 6 s'appuie lui-même sur des langages de recherche tels que Lustre [6] et Lucid Synchrone [16]. Vélus intègre un compilateur produisant du code impératif Clight, langage d'entrée du compilateur vérifié CompCert [13], ainsi qu'une sémantique à flots de données pour son langage d'entrée, et une preuve de bout en bout mettant en relation cette sémantique et celle du code assembleur généré.

Dans cet article, on ajoute à Vélus deux nouvelles structures d'activation présentes dans Lucid Synchrone [7] et Scade 6 [9] : le *switch*, et le bloc de déclarations locales. La sémantique à flots de données du langage source de Vélus est étendue pour traiter ces constructions. De précédents travaux se sont concentrés sur la preuve de correction du schéma de compilation de Vélus. On a étendu ces preuves pour traiter le *switch* et les déclarations locales. Dans cet article, on s'intéresse plutôt à la preuve de propriétés dynamiques du modèle sémantique, comme l'adéquation des flots calculés aux définitions statiques d'un programme (typage des valeurs et échantillonage), ou son déterminisme : pour une entrée donnée, une seule sortie est possible. Ces propriétés dépendent de la bonne formation du programme et en particulier de l'absence de cycle de dépendance dans ses définitions. L'encodage de cette notion de dépendance dans Coq est rendue plus complexe par l'ajout de structures d'activation.

**Un exemple : contrôle des portes d'une télécabine** On présente un programme Lustre contrôlant l'ouverture et la fermeture de la porte d'une télécabine hypothétique. Un moteur pas à pas bipolaire est utilisé pour déplacer les portes le long de leurs rails. Le tableau de la figure 1 indique le signal à appliquer à chacun des pôles du moteur pour le faire tourner dans le sens horaire. Ce comportement peut être implémenté dans Vélus à l'aide de deux équations utilisant chacune l'opérateur de délai initialisé *fby*. Pour faire tourner le moteur dans le sens anti-horaire, il faut inverser cette séquence d'activation. Le nœud *control_moteur* gère ce contrôle de bas
<figure><img src="image_57.png" /><figcaption>FIGURE 1 – Séquence de contrôle des moteurs</figcaption></figure>

```pascal
type moteurDir = Ouvre | Ferme | Bloque

node control_moteur dir : moteurDir returns (moteurA, moteurB : bool)
let
  switch dir
  | Ouvre do
    moteurA = true fby (not moteurB);
    moteurB = true fby moteurA;
  | Ferme do
    moteurA = true fby moteurB;
    moteurB = true fby (not moteurA);
  | Bloque do
    (moteurA, moteurB) = (false, false);
end
tel
```

<caption>FIGURE 2 – Contrôle des moteurs</caption>

niveau. La structure d'activation **switch** active le bon comportement en fonction du paramètre **dir**, dans le sens horaire pour **Ouvre**, anti-horaire pour **Ferme**, ou stoppé pour **Bloque**.

Ce nœud est instancié par le nœud **control_porte**, présenté en figure 3, qui choisit la direction des moteurs. Quand la cabine est en dehors de la station, les portes sont fermées. La station est équipée de 8 repères fixés au rail. Quand la cabine passe un repère, l'entrée **repere** vaut **true**. Les portes doivent s'ouvrir entre les repères 1 et 3, rester ouvertes jusqu'au repère 6, puis se fermer avant le repère 8. Le compteur **nbRepere** est déclaré localement à la branche **true** du **switch**. Il est incrémenté chaque fois qu'un repère est détecté, jusqu'à 8. Pour le mettre à jour, on utilise la construction **last**, introduite dans [8], qui permet d'accéder à la valeur précédente d'un flot, même calculée dans l'autre branche du **switch** interne. La déclaration **last** doit être accompagnée d'une expression d'initialisation, pour donner une valeur à **last nbRepere** au premier instant.

Un fabriquant de capteurs (hypothétique également) propose d'ajouter une redondance permettant de vérifier si les portes peuvent être ouvertes sans danger. Pour cela, il faut que la cabine soit proche du sol et que sa vitesse verticale soit suffisamment faible. Un capteur infrarouge placé sous la cabine permet de mesurer la distance avec le sol. Le manque de visibilité (neige, brouillard) peut parfois empêcher le capteur de fonctionner correctement pendant le trajet de la cabine. Pour pallier à ce problème, un accéléromètre permet de mesurer l'accélération verticale de la cabine. Cette mesure est alors intégrée pour calculer la vitesse courante, puis la position verticale. L'inconvénient de ce deuxième capteur est que de petites erreurs de mesure peuvent faire dériver l'estimation. Le nœud **ouvrir_ok** combine donc les données de ces capteurs pour vérifier que la porte peut être ouverte sans danger. Si le capteur infrarouge n'est pas
```pascal
node control_porte(enStation: bool; repere: bool) returns (moteurA, moteurB: bool)
var dir: moteurDir;
let
  switch enStation
  | true do
    var last nbRepere: int = 0;
    let
      switch repere
      | true do nbRepere = (last nbRepere + 1) mod 8;
      | false do nbRepere = last nbRepere
    end;
    dir = if nbRepere > 0 and nbRepere < 3 then Ouvre else if nbRepere > 5 then Ferme else Bloque;
  tel
  | false do dir = Bloque;
end;
(moteurA, moteurB) = control_moteur dir;
tel
```

<figure><img src="image_58.png" /><figcaption>FIGURE 3 – Contrôle des portes</figcaption></figure>

disponible, la valeur de `captdist` est négative et on utilise alors la valeur de l'accéléromètre `accely`. On note que les dépendances de ce programme commutent : dans la branche `true`, `vy` dépend de `y`, alors que c'est le contraire dans la branche `false`.

```pascal
node ouvrir_ok(y_max, vy_max, captdist, accely, dt: double) returns (ok: bool)
var last vy: double = 0.0; last y: double = 0.0;
let
  switch (captdist > 0.0)
  | true do
    y = captdist;
    vy = (y - last y) / dt;
  | false do
    vy = last vy + accely * dt;
    y = last y + vy * dt;
end;
ok = y < y_max and vy < vy_max;
tel
```

<caption>FIGURE 4 – Vérification de la position et vitesse de la cabine</caption>

La suite présente une formalisation de la sémantique du `switch` et des déclarations locales dans Vélus. La section 3 adapte l'analyse de dépendance introduite dans [5, §2.3], et détaille son implémentation en Coq. On s'intéresse particulièrement au traitement des déclarations locales et de la commutation de dépendance. En section 4, on détaille le schéma d'induction introduit dans [5, §2.3], qu'on applique pour prouver que la sémantique de Vélus est déterministe.

La documentation du développement Coq décrit dans cet article, ainsi qu'une démonstration de l'exemple présenté ci-dessus sont accessibles à https://velus.inria.fr/jfla2023.

## 2 Sémantique à flots de données de Vélus

La syntaxe abstraite du langage d'entrée de Vélus est présentée en figure 5. Le langage des expressions étend celui présenté en [5]. Une expression peut faire référence à une constante primitive `c` ou énumérée `C`, un flot nommé avec `x`, et à sa valeur précédente avec `last x`. Les
opérateurs unaires et binaires arithmétiques et logiques habituels sont disponibles. Le fby introduit un délai initialisé par les expressions à sa gauche. La flèche d'initialisation -> permet de donner une valeur particulière à l'instant initial. Le when échantillonne son premier argument selon la valeur d'un flot énuméré, et le merge fusionne des flots échantillonnés complémentaires. L'opérateur case est une généralisation de if-then-else pour une condition énumérée. Pour ces cinq dernières constructions, chaque opérande peut contenir une liste (non-vide) de sous-expressions (notée e⁺); cela permet à une expression de définir plusieurs flots. Une expression peut enfin appeler un autre nœud du programme. Le compilateur supporte aussi le reset modulaire, traité formellement dans [4].

Dans [5], un bloc peut seulement définir une équation. On ajoute les structures d'activation switch, et les déclarations locales. Chaque déclaration est annotée par son type et son horloge statique. On y ajoute, pendant l'élaboration du programme, une étiquette unique pour chaque flot, ou deux pour un flot défini avec last. Par ailleurs, chaque branche d'un switch est annotée par une fonction de renommage de ces étiquettes σ. On verra plus loin comment ces étiquettes sont utilisées lors de l'analyse de dépendance d'un programme. Chaque nœud contient un bloc et spécifie ses entrées et sorties. Un programme est constitué d'une liste de définitions de types énumérés, suivie d'une liste non vide de nœuds.

<figure><img src="image_59.png" /><figcaption>FIGURE 5 – Syntaxe abstraite de Lustre</figcaption></figure>

## 2.1 Noyau du langage

On s'intéresse maintenant au modèle sémantique de Vélus, défini par un ensemble de règles, encodées comme des prédicats inductifs sur la syntaxe abstraite. Ce modèle contraint des flots infinis, représentés en Coq par le type co-inductif Stream A := Cons : A → Stream A → Stream A. Dans la suite, on note $x \cdot xs$ pour Cons x xs. Ces flots étant infinis, on utilise la relation d'équivalence entre flots $\equiv$ de la bibliothèque standard, dont la définition est rappelée ci-dessous.

**Définition 1 (Equivalence de flots).**

$$x \cdot xs \equiv y \cdot ys \quad ssi \quad x = y \quad et \quad xs \equiv ys$$

On rappelle d'abord le modèle sémantique de Vélus déjà présenté dans [5]. Ces règles encodent, sous forme de relation entre flots, la sémantique décrite dans [10]. On présente en figure 6 les règles centrales de ce modèle. Le jugement $G, H, bs \vdash e \Downarrow vss$ se lit « sous l'environnement global G, l'historique H et l'horloge de base bs, l'expression e produit les flots vss ». Comme dit plus
haut, une expression peut produire plusieurs flots, et vss est donc une liste. Dans les règles suivantes, on note $[vs]$ quand cette liste ne contient qu'un élément. L'historique $H$ associe un flot à chaque entrée, sortie et déclaration locale du nœud. Dans la suite, on note $x \in \text{dom}(H)$ le jugement « il y a un flot associé à $x$ dans $H$ ». Si c'est le cas, $H(x)$ est défini comme le flot associé à $x$ dans $H$. La première règle de figure 6 indique que, pour donner une sémantique à l'expression $x$, on lit le flot associé à $x$ dans l'historique.

Un flot peut être échantillonné, c'est-à-dire que ses valeurs ne sont pas toujours présentes. Dans Vélus, on caractérise explicitement les absences (notées $\langle \rangle$) et présences (notées $\langle v \rangle$). Le « rythme » d'un flot échantillonné est caractérisé par un flot booléen, son horloge. L'horloge de base $bs$ est celle des flots les plus rapides du nœud. La fonction base-of permet de la calculer : elle est vraie à un instant si et seulement si au moins une entrée du nœud est présente. Intuitivement, le nœud est actif à chaque fois qu'au moins l'une de ses entrées est présente. L'horloge $bs$ est utilisée par la deuxième règle pour donner le rythme d'une constante avec la fonction const.

Le jugement $G, H, bs \vdash blk$ indique que la sémantique d'un bloc *blk* peut être donnée sous le contexte $G, H, bs$. Un bloc ne produit pas de valeur, mais induit un ensemble de contraintes sur l'historique $H$. La règle pour l'équation est rappelée en figure 6 : les valeurs associées aux noms à gauche de l'équation doivent être celles calculées par les expressions à droite.

Enfin, l'environnement global $G$ contient l'ensemble des nœuds du programme. Pour donner la sémantique d'un nœud de $G$, il faut donner un historique $H$ respectant les contraintes des blocs du nœud. Les flots associés aux entrées et sorties du nœud sont lus dans $H$.

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\begin{array}{@{}c@{\,}c@{\,}c@{\,}c@{}}
  H(x) & \equiv & vs & \\
  \multicolumn{1}{@{}c@{}}{\overline{\phantom{H(x) \equiv vs}}} & & & \\
  G, H, bs \vdash & x & \Downarrow & [vs] \\
\end{array}
&
\begin{array}{@{}c@{\,}c@{\,}c@{\,}c@{}}
  \overline{\phantom{G, H, bs \vdash}} & c & \Downarrow & [const\,bs\,c] \\
  G, H, bs \vdash & c & \Downarrow & [const\,bs\,c] \\
\end{array}
&
\begin{array}{@{}c@{\,}c@{\,}c@{\,}c@{}}
  \text{const} & (T \cdot bs) & c & \equiv & \langle c \rangle \cdot \text{const}\,bs\,c \\
  \text{const} & (F \cdot bs) & c & \equiv & \langle \rangle \cdot \text{const}\,bs\,c \\
\end{array} \\
\\
\begin{array}{@{}c@{\,}c@{\,}c@{\,}c@{}}
  \frac{
    \begin{array}{@{}c@{\,}c@{}}
      G, H, bs \vdash & es \Downarrow & (vs_1, \dots, vs_n) \\
      \phantom{G, H, bs \vdash} & & \\
      G, H, bs \vdash & (x_1, \dots, x_n) & = & es
    \end{array}
  }{
    \forall i \in 1 \dots n, H(x_i) \equiv vs_i
  } & & \\
\\
\begin{array}{@{}c@{\,}c@{\,}c@{\,}c@{}}
  \frac{
    \begin{array}{@{}c@{\,}c@{}}
      G(f) & = & \text{node } f(x_1, \dots, x_n) \text{ returns } (y_1, \dots, y_m) \text{ blk} \\
      \phantom{G(f) =} & & \\
      \forall i \in 1 \dots n, H(x_i) & \equiv & xs_i
    \end{array}
  }{
    \forall i \in 1 \dots m, H(y_i) \equiv ys_i
  } & & \\
  \frac{
    \begin{array}{@{}c@{\,}c@{}}
      G, H, (\text{base-of}(xs_1, \dots, xs_n)) & \vdash & blk \\
      \phantom{G, H, (\text{base-of}(xs_1, \dots, xs_n))} & & \\
      G \vdash & f(xs_1, \dots, xs_n) & \Downarrow (ys_1, \dots, ys_m)
    \end{array}
  }{
    \forall i \in 1 \dots m, H(y_i) \equiv ys_i
  } & & \\
\end{array}
\end{array}
$$

<caption>FIGURE 6 – Règles sémantiques centrales [5]</caption>

La sémantique de chaque autre opérateur du language d'expressions est exprimée au moyen d'une fonction de flots. On donne ici l'exemple de l'opérateur de délai initialisé *fby*, qui permet d'accéder à la valeur des flots aux instants précédents. Ce fonctionnement est encodé par les opérateurs *fby* et *fby1*, présentés en figure 7. La première valeur présente du flot de gauche est produite par *fby*, tandis que les valeurs du deuxième flot sont conservées dans le premier argument de *fby1* jusqu'à la présence suivante. Pour donner une sémantique à l'expression *es0 fby es1*, on distribue l'opérateur *fby* sur les flots produits par les sous-expressions.

On note que l'opérateur *fby* est insensible aux absences, c'est à dire qu'on peut en insérer ou supprimer sans changer son comportement fondamental. Il prend une valeur du flot de gauche et l'ajoute devant le flot de droite. Cette idée s'étend aux nœuds, qui associent aux absences en entrée des absences en sortie. Les nœuds sont donc eux aussi insensibles aux absences.
<figure><img src="image_60.png" /><figcaption>FIGURE 7 – Sémantique de l’opérateur de délai initialisé fby</figcaption></figure>

<figure><img src="image_61.png" /><figcaption>FIGURE 8 – Sémantique du switch</figcaption></figure>

## 2.2 Structure d'activation switch

Pour modéliser la sémantique du `switch`, on s'appuie sur l'idée d'insensibilité aux absences présentée ci-dessus. Une branche doit être insensible, dans le même sens que pour les `fby` et les nœuds, quand l'expression de garde ne correspond pas à l'étiquette de la branche. De plus, le `switch` doit combiner les flots produits par les branches, en choisissant à chaque instant les valeurs de la branche désignée par l'expression de garde, les valeurs de toutes les autres branches étant absentes. Dans les instants ou l'expression de garde est absente, toutes les valeurs de toutes les branches sont absentes.

On concrétise ces intuitions par la règle du `switch` définie en figure 8, à gauche. L'opérateur `when`, appliqué à l'historique et à l'horloge de base, est au cœur de cette modélisation. Pour chaque branche, il est appliqué avec le flot de l'expression de garde `cs` et l'étiquette `Cᵢ` de la branche. Ainsi, il rend la branche insensible quand le flot de garde ne correspond pas à l'étiquette, et ne reporte les valeurs produites par la branche que quand elles sont présentes.

La définition de `when` pour un flot est donnée en figure 8, à droite. C'est une fonction partielle : ses deux entrées doivent être présentes en même temps. Pour appliquer `when` à l'horloge de base, un flot booléen sans absence explicite, ce critère est relaxé, et on interprète les absences dans le flot produit par `when` comme le booléen `false`. Les historiques étant représentés comme des fonctions partielles, on peut définir `when` appliqué à un historique par `(when$^C$ H cs)(x) = when$^C$ (H(x)) cs`. Cela signifie que `(when$^C$ H cs)(x)` est défini si et seulement si le flot associé à `x` dans `H` a le même rythme que `cs`. Ainsi, la sémantique des sous-blocs du `switch` est donnée dans un environnement plus restreint que `H`. Cela correspond d'ailleurs à un critère de typage statique du langage, que nous ne détaillerons pas ici.

## 2.3 Déclarations locales

Comme on l'a vu dans les exemples, l'utilisateur peut arbitrairement imbriquer des déclarations locales, y compris dans la branche d'un `switch`. On introduit en figure 10 une définition pour la sémantique d'un bloc de déclarations locales. La première prémisse de la règle spécifie le domaine d'un historique local `H'` qui associe un flot à chaque déclaration locale du bloc. Cet historique `H'` vient compléter l'historique global `H` pour donner une sémantique aux sous-blocs, comme indiqué dans la troisième prémisse. Cette formalisation est inspirée de celle présentée
dans [7, §3.2]. L'opérateur d'union d'historique + est défini par

$$ (H_1 + H_2)(x) = \begin{cases} H_2(x) & \text{si } x \in \text{dom}(H_2) \\ H_1(x) & \text{sinon.} \end{cases} $$

Le cas où $x \in \text{dom}(H_1)$ et $x \in \text{dom}(H_2)$ ne peut en fait pas se produire, puisque Vélus rejette statiquement le masquage d'une déclaration globale par une déclaration locale. Dans le cas contraire, on pourrait écrire le programme de la figure 9, où la variable x dont dépend l'horloge de y est masquée. Pour éviter ce problème, il serait nécessaire d'introduire un niveau d'indirection dans les types d'horloges [8, Fig. 3], ce qu'on n'a pas fait dans Vélus.

```c
node f(x : bool; y : int when x) returns (z : int)
var x : int;
let
    x = y + 1;
    z = x;
tel
```

<caption>FIGURE 9 – Programme avec masquage, rejeté par Vélus</caption>

## Variables partagées
Les flot locaux peuvent être déclarés comme partagés en utilisant le mot clé `last`. Pour traiter cette fonctionnalité, la définition d'historique est enrichie pour associer un flot différent à x et à `last x`, comme dans [17] ; on y accède respectivement avec $H(x)$ et $H(last x)$. Dans le développement Coq, l'historique est encodé par une paire d'environnements, l'un pour les variables courantes et l'autre pour les `last`. Les règles de sémantique pour `last` sont présentées en figure 10. La deuxième règle indique que l'expression `last x` produit le flot associé à `last x` dans l'historique. Cette association est contrainte au point de définition de x par la première règle. Le flot associé à `last x` correspond à celui associé à x, retardé par un délai initialisé par le flot de l'expression d'initialisation e.

$$ \frac{\begin{array}{l} \forall x, x \in \text{dom}(H') \iff x \in \text{locs} \\ \forall x e, (\text{last } x = e) \in \text{locs} \implies G, H + H', bs \vdash \text{last } x = e \quad G, H + H', bs \vdash \text{blks} \\ \hline G, H, bs \vdash \text{var } \text{locs} \text{ let } \text{blks } tel \end{array}}{\begin{array}{l} \displaystyle \frac{H(\text{last } x) \equiv vs}{G, H, bs \vdash \text{last } x \Downarrow [vs]} \\ \\ \displaystyle \frac{G, H + H', bs \vdash e \Downarrow [vs_0]}{G, H + H', bs \vdash \text{last } x = e} \qquad H'(x) \equiv vs_1 \qquad H'(\text{last } x) \equiv \text{fby } vs_0 \ vs_1 \end{array}} $$

<caption>FIGURE 10 – Sémantique des déclarations locales et `last`</caption>

# 3 Analyse de dépendance

Dans la section précédente, on a présenté la sémantique dynamique de Vélus. Cependant, ce modèle seul ne suffit pas à garantir les propriétés attendues du langage. Considérons l'équation
x = x. Un nœud la contenant ne serait pas déterministe, puisqu'elle n'applique aucune contrainte au flot associé à x, qui peut prendre n'importe quelle valeur. A l'inverse, l'équation x = x + 1 n'admet pas de sémantique, alors qu'elle est bien typée. De plus, de telles équations ne peuvent pas être compilées, puisque dans le code impératif produit, une valeur doit être calculée avant son utilisation. C'est aussi le cas pour les systèmes d'équations contenant un cycle, comme par exemple, x = y + 1; y = x * 2.

De nombreux travaux se sont penchés sur l'analyse statique de ces dépendances. Les analyses les plus fines [12, 1, 9] les modélisent sous forme de systèmes de types. Ces formulations permettent de donner à un nœud un type indiquant les dépendances entre entrées et sorties. Elles peuvent par exemple accepter l'équation (x, y) = f(x) si la première sortie de f ne dépend pas instantanément de son entrée. Le schéma de compilation doit alors être adapté pour produire un programme ordonnançable, soit en expansant les appels de nœud [9], soit en les décomposant en plusieurs appels ordonnançables séparément [18, 14]. Le schéma de compilation de Vélus est bien plus simple : chaque nœud est une « boite noire », et les appels sont atomiques [2]. L'exemple est donc rejeté. L'analyse de dépendance de Vélus introduite dans [5, §2.3] est basée sur une analyse de graphe. Dans cette section, on étend cette analyse pour traiter les nouvelles structures d'activation, et on décrit l'implémentation Coq de l'algorithme d'analyse de graphe.

## 3.1 Règles de dépendances pour le langage

A chaque flot x du programme est associé une étiquette $\alpha_x$. Cette indirection permet de donner une étiquette différente à deux déclarations locales utilisant le même nom. La suite définit d'abord la fonction calculant l'ensemble des variables utilisées instantanément dans une expression avant de présenter formellement la relation de dépendance entre deux étiquettes.

### 3.1.1 Variables utilisées instantanément

Pour analyser les cycles de dépendance dans un programme, il faut d'abord déterminer l'ensemble de variables utilisées par une expression. Considérons l'équation x = 0 fby (x + 1). Elle ne doit pas induire de cycle de dépendance puisque x ne dépend que de sa valeur précédente. On ne s'intéressera donc qu'aux variables utilisées instantanément dans une expression, c'est-à-dire celles n'apparaissant pas à droite d'un fby.

Une fonction pour ce calcul est proposée dans [2, Fig. 3], mais ne s'applique que sur un programme normalisé. Notre analyse doit être un peu plus précise pour traiter le langage général. Par exemple, l'équation (x, y) = if c then (0, x) else (1, 0) ne contient pas de cycle : y dépend de x, mais x ne dépend pas de lui même. Effectivement, cette équation est normalisée [5] en deux équations x = if c then 0 else 1 et y = if c then x else 0, dans lesquelles l'absence de cycle est évidente. Pour traiter cette subtilité, on définit la fonction UsedInst<sub>Γ</sub>(e)[k] qui collecte les étiquettes des variables utilisées instantanément pour définir le k-ième flot produit par l'expression e. Dans cet exemple, k = 0 désigne la définition x = if c then 0 else 1, et k = 1 désigne la définition y = if c then x else 0. L'environnement Γ associe le nom d'un flot à son étiquette. Il est construit à partir des déclarations encodées dans la syntaxe abstraite.

On donne en figure 11 quelques cas intéressants de la définition de cette fonction, qui est encodée comme un prédicat inductif comme dans le développement Coq. Pour une variable, on récupère l'annotation correspondante dans l'environnement. Pour une expression composée comme le if-then-else, on considère le flot de la condition, et les k-ième flots des deux alternatives. Pour traiter une liste de sous expressions, il faut choisir le k-ième élément de la liste aplatie des flots. Pour cela, on calcule le nombre de flots de chaque expression avec
<figure><img src="image_62.png" /><figcaption>FIGURE 11 – Quelques règles pour UsedInst</figcaption></figure>

numstreams(e). Pour un fby, on ne prend pas en compte les variables apparaissant à droite, comme expliqué plus tôt. Enfin, un appel de nœud est atomique : l'expression f(es) dépend de toutes les variables utilisées instantanément dans es.

### 3.1.2 Variables définies et dépendances

On souhaite maintenant établir les contraintes de dépendance induites par un bloc. On note $\Gamma \vdash blk | \alpha_2 \leftarrow^{dep} \alpha_1$ pour indiquer que sous l'environnement $\Gamma$, dans le bloc *blk*, $\alpha_2$ dépend de $\alpha_1$. Les règles qui définissent ces contraintes dépendent aussi d'une fonction $Def_\Gamma(blk)$ qui calcule les étiquettes définies par un bloc *blk*.

**Equations** : Les étiquettes définies par une équation sont celles des variables à gauche de l'équation. Une équation induit immédiatement une dépendance entre l'étiquette du *k*-ième flot défini, et les variables utilisées instantanément dans le *k*-ième flot des expressions. Par exemple, dans $(x, y) = (0, x \text{ fby } z)$, $x$ ne dépend d'aucune étiquette et $y$ dépend seulement de $x$.

$$ \frac{\Gamma(x_i) = \alpha_{x_i}}{\alpha_{x_i} \in Def_{\Gamma}((x_1, \dots, x_n) = es)} \qquad \frac{\Gamma(x_i) = \alpha_{x_i} \quad \alpha \in \text{UsedInst}_{\Gamma}(es)[i]}{\Gamma \vdash (x_1, \dots, x_n) = es \mid \alpha_{x_i} \leftarrow^{dep} \alpha} $$

<caption>FIGURE 12 – Etiquettes définies et dépendances pour une équation</caption>

**Déclarations locales** : Les déclarations locales introduisent de nouvelles étiquettes *locs*. Pour traiter les sous-blocs d'une déclaration, il faut les prendre en compte, en étendant l'environnement avec +, défini comme : $\forall x, (\Gamma + locs)(x) = \alpha_x \leftrightarrow (\Gamma(x) = \alpha_x \lor locs(x) = \alpha_x)$. Les règles de calcul de *Def* et de dépendance utilisant cet opérateur sont données en figure 13. On note que les étiquettes d'une déclaration locale échappent à leur portée. C'est nécessaire pour construire un graphe de dépendance global au nœud. Un invariant statique, non présenté ici, garantit par ailleurs que toutes les étiquettes du nœud sont distinctes.
$$ \frac{\alpha \in \mathrm{Def}_{\Gamma+\mathrm{locs}}(\mathrm{blks})}{\alpha \in \mathrm{Def}_{\Gamma}(\mathrm{var \, locs \, let \, blks \, tel})} \qquad \frac{(\Gamma + \mathrm{locs}) \vdash \mathrm{blks} \mid \alpha_y \underset{\alpha_x}{\stackrel{\mathrm{dep}}{\rightleftarrows}}}{\Gamma \vdash \mathrm{var \, locs \, let \, blks \, tel} \mid \alpha_y \underset{\alpha_x}{\stackrel{\mathrm{dep}}{\rightleftarrows}}} \\ \frac{(\mathrm{last} \ y : (\alpha_y, \alpha_{\mathrm{lasty}}) = e) \in \mathrm{locs}}{\Gamma \vdash \mathrm{var \, locs \, let \, blks \, tel} \mid \alpha_{\mathrm{lasty}} \underset{\alpha_x}{\stackrel{\mathrm{dep}}{\rightleftarrows}}} \qquad \alpha_x \in \mathrm{UsedInst}_{(\Gamma+\mathrm{locs})}(e)[0] $$

<caption>FIGURE 13 – Etiquettes définies et dépendances pour une déclaration locale</caption>

**Last**: Si l'utilisateur déclare un flot local x avec une valeur **last** initiale, on ajoute également une étiquette distincte pour **last** x. Cela permet de traiter **last** x comme un flot à part, qui ne dépend que des flots apparaissant dans son expression d'initialisation. Ainsi, les blocs présentés en figure 14 sont valides (mais ne produisent pas le même flot pour x). En revanche, celui présenté en figure 15 ne l'est pas, puisque x dépend immédiatement de **last** x et inversement.

var last x = 0;
let x = last x + 1; tel

var last x = x + 1;
let x = 0; tel

var last x = x + 1;
let x = last x; tel

<caption>FIGURE 14 – Déclarations **last** correctes</caption>

<caption>FIGURE 15 – Déclaration **last** cyclique</caption>

**Switch-Case**: Le cas du switch est plus complexe. On rappelle le nœud présenté en figure 4. Il ne serait pas accepté si on associait les étiquettes $\alpha_y$ et $\alpha_{vy}$ à y et vy respectivement : il y aurait un cycle. On peut en revanche associer des étiquettes $\alpha_{y_T}$ et $\alpha_{y_F}$ aux définitions de y dans les branches **true** et **false**, et de même pour vy. Les deux branches étant mutuellement exclusives, il ne peut pas y avoir d'interaction entre $\alpha_{y_T}$ et $\alpha_{y_F}$. L'étiquette $\alpha_y$ dépend par contre de ces étiquettes locales aux branches. De même, tous ces flots dépendent de la condition qui détermine quelle branche est activée, et donc de $\alpha_{captdist}$. Le graphe de dépendance pour l'exemple est présenté en figure 16. Il est bien acyclique.

<figure><img src="image_63.png" /><figcaption>FIGURE 16 – Graph de dépendance pour la figure 4</figcaption></figure>

Pour encoder ces changements d'associations, chaque branche d'un **switch** est annotée dans la syntaxe abstraite par une fonction $\sigma$ qui s'applique à l'environnement pour modifier les étiquettes. On omet cette annotation dans la présentation des règles où elle n'est pas utile. Un invariant statique non présenté ici nous garantit que les étiquettes renommées par $\sigma$ sont celles
des flots définis par le **switch**. On a

$$ \sigma(\Gamma)(x) = \begin{cases} \sigma(x) & \text{si } x \in \sigma \\ \Gamma(x) & \text{sinon.} \end{cases} $$

La figure 17 présente les règles de dépendances pour le **switch**. Les étiquettes définies par un **switch** sont celles des sous-blocs après renommage par $\sigma$. La deuxième règle y ajoute les étiquettes correspondantes avant le renommage. La fonction $\sigma$ est aussi utilisée pour calculer les dépendances des sous-blocs. Toutes les étiquettes des flots définis par le **switch** dépendent de la condition. La dernière règle ajoute une dépendance entre chaque étiquette interne $\alpha_x$ et l'étiquette correspondante externe $\alpha_y$, pour « connecter » les flots définis.

Cet étiquetage reflète le schéma de compilation présenté dans [8]. Une nouvelle variable est introduite pour chaque variable définie et chaque branche, et un **merge** combine les valeurs de ces nouvelles variables pour définir la variable originale.

$$ \frac{\alpha \in \text{Def}_{\sigma_i(\Gamma)}(\text{blks}_i)}{\alpha \in \text{Def}_{\Gamma}(\text{switch } e(C_i \text{ do } \sigma_i \text{ blks}_i)_i \text{ end})} \qquad \frac{x \in \sigma_i \quad \Gamma(x) = \alpha}{\alpha \in \text{Def}_{\Gamma}(\text{switch } e(C_i \text{ do } \sigma_i \text{ blks}_i)_i \text{ end})} \\ \frac{\sigma_i(\Gamma) \vdash \text{blks}_i \mid \alpha_1 \stackrel{\text{dep}}{\leftarrow} \alpha_2}{\Gamma \vdash \text{switch } e(C_i \text{ do } \sigma_i \text{ blks}_i)_i \text{ end} \mid \alpha_1 \stackrel{\text{dep}}{\leftarrow} \alpha_2} \\ \frac{\alpha_x \in \text{UsedInst}_{\Gamma}(e)[0]}{\alpha_y \in \text{Def}_{\Gamma}(\text{switch } e(C_i \text{ do } \text{blks}_i)_i \text{ end})} \qquad \frac{\Gamma \vdash \text{switch } e(C_i \text{ do } \text{blks}_i)_i \text{ end} \mid \alpha_y \stackrel{\text{dep}}{\leftarrow} \alpha_x}{\alpha_x \in \text{UsedInst}_{\Gamma}(e)[0] \mid \alpha_y \in \text{Def}_{\Gamma}(\text{switch } e(C_i \text{ do } \text{blks}_i)_i \text{ end})} \\ \frac{x \in \sigma_i \quad \Gamma(x) = \alpha_y \quad \sigma_i(\Gamma)(x) = \alpha_x}{\Gamma \vdash \text{switch } e(C_i \text{ do } \sigma_i \text{ blks}_i)_i \text{ end} \mid \alpha_y \stackrel{\text{dep}}{\leftarrow} \alpha_x} $$

<caption>FIGURE 17 – Etiquettes définies et dépendances pour un **switch**</caption>

## 3.2 Analyse du graphe de dépendance

Les relations de dépendance décrites plus haut nous permettent de construire le graphe de dépendance d'un programme. On exprime ce graphe en Coq par une table associant chaque étiquette à la liste de ses prédécesseurs. Cette représentation ne garantit bien sûr pas l'absence de cycles dans le graphe. C'est le prédicat inductif AcyGraph, introduit dans [5], qui caractérise les graphes acycliques. Il est défini par les trois règles rappelées dans la figure 18. Ce prédicat est paramétré par un ensemble de sommets et un ensemble d'arcs. Un graphe vide est acyclique. Ajouter un sommet préserve l'acyclicité. Cependant, on ne peut ajouter un arc entre deux sommets $\alpha_x$ et $\alpha_y$ que s'ils sont distincts, et qu'il n'existe pas d'arc retour dans la clôture transitive des arcs existants.

On veut maintenant développer une fonction vérifiant qu'un graphe de dépendance construit selon les règles de la section 3.1 satisfait le prédicat d'acyclicité. On s'appuie sur un algorithme bien connu de recherche en profondeur pour traverser les prédécesseurs de chaque sommet dans le graphe. Pour justifier de sa terminaison et de sa correction, on utilise les types dépendants de Coq pour encoder les invariants de l'algorithme. On utilise l'extension Program [19] qui permet
<figure><img src="image_64.png" /><figcaption>FIGURE 18 – Graphe acyclique par construction</figcaption></figure>

de définir la partie calculatoire de l'algorithm e en Gallina, le language de programmation à la
ML de Coq, et de traiter séparément les obligations de preuve avec le langage de tactiques Ltac.

On s'intéresse d'abord à la partie calculatoire, présentée figure 19, en ignorant les types
dépendants utilisés pour les entrées et sorties. L'appel dfs' s x v recherche récursivement les
prédécesseurs de x dans le graph. Elle renvoie l'ensemble des sommets visités à l'issue de son
exécution. L'ensemble v représente les sommets déjà visités. L'ensemble s contient les sommets
sur le chemin parcouru depuis le sommet initial. Ces ensembles sont représentés par le type PS.t.
On utilise la monade option pour représenter la réussite ou l'échec de l'algorithm e. La fonction
échoue (ligne 13) si elle rencontre un sommet x ∈ s, ce qui signifie qu'il y a un cycle dans le graphe.
Sinon, si x ∈ v, c'est qu'on connaît déjà tous ses prédécesseurs, donc on peut renvoyer v (ligne 16).
Si x reste à traiter, on récupère la liste de ses prédécesseurs (ligne 18), et on appelle récursivement
dfs' sur chacun, après avoir ajouté x à s (ligne 21). Pour itérer sur la liste des prédécesseurs,
on utilise ofold_left : (B → A → option B) → list A → option B → option B, qui se
comporte comme fold_left, mais s'interrompt si la fonction retourne une erreur (ligne 22).

Aux lignes 12 et 15, on utilise la construction match/with, plutôt qu'un if/then/else pour
traiter la condition booléenne. C'est une contrainte liée à l'utilisation de Program qui, si on utilise
if/then/else, ne conserve pas assez d'information dans les obligations de preuves générées.

**Terminaison :** La fonction *dfs'* ne respecte pas le critère de récursion gardée de Coq où chaque appel récursif doit être effectué sur un sous terme de l'argument initial. On utilise *Program Fixpoint* pour définir une fonction récursive en utilisant une « mesure », c'est-à-dire une fonction des arguments vers un entier naturel. Si cette mesure décroît strictement à chaque appel récursif, la fonction termine, puisque (N, ≤) est bien fondé. Pour cet algorithme, on sait que l'ensemble *s* grandit à chaque appel récursif, et qu'il est inclus dans l'ensemble des sommets du graphe. La mesure *numRemaining*, définie ligne 3 décroît donc strictement.

**Correction :** L'algorithm e est correct si sa réussite indique qu'un témoin d'AcyGraph peut être associé au graphe analysé. Il est difficile de raisonner à posteriori sur un programme écrit avec *Program Fixpoint*, car le programme Coq généré contient des termes complexes justifiant de sa terminaison. À la place, on intègre les invariants de l'algorithm e dans le type de la fonction.

L'invariant *visited s v* garantit d'abord que l'ensemble *s* des sommets dans le parcours et l'ensemble *v* des sommets visités sont bien disjoints (ligne 6). Par ailleurs, il indique qu'il existe un ensemble d'arcs *a*, tel que (1) le graphe formé par les sommets *v* et les arcs *a* est acyclique, et (2) pour chaque sommet *x* de *v*, tout arc allant vers *x* dans le graph analysé est présent dans *a*, ce qui est caractérisé par *has_arc*. Intuitivement, cela indique que le sous-graphe de graph réduit aux sommets de *v* est effectivement acyclique. On note que l'ensemble d'arcs *a* n'a pas besoin d'être calculé explicitement. Un tel existentiel disparaîtra dans le code OCaml extrait et ne coûtera donc pas de temps ni de mémoire à l'exécution. Par ailleurs, le type de *dfs'* garantit que le sommet *x* recherché est bien dans l'ensemble *v'* renvoyé, qui est un sur-ensemble de celui passé en entrée à la fonction.

Itérer *dfs* sur l'ensemble des sommets du graphe permet donc de construire un témoin
AcyGraph pour l'ensemble des sommets du graphe. A chaque nœud du programme source analysé,
1 Variable graph : Env.t (list label).
2
3 Definition numRemaining (s : PS.t) : nat := Env.cardinal graph — PS.cardinal s.
4
5 Definition visited (s : PS.t) (v : PS.t) : Prop :=
6 (∀ x, PS.In x s → ¬PS.In x v)
7 ∧ ∃a, AcyGraph v a ∧ (∀ x, PS.In x v → ∃zs, Env.find x graph = Some zs ∧ (∀ y, In y zs → has_arc a y x)).
8
9 Program Fixpoint dfs' (s : { p | ∀x, PS.In x p → Env.In x graph }) (x : ident)
10 (v : { v | visited s v }) {measure (numRemaining s)}
11 : option { v' | visited s v' & PS.In x v' ∧ PS.Subset v v' } :=
12 match PS.mem x s with
13 | true ⇒ None
14 | false ⇒
15 match PS.mem x v with
16 | true ⇒ Some (exist2 _ _ v _ _)
17 | false ⇒
18 match Env.find x graph with
19 | None ⇒ None
20 | Some zs ⇒
21 let s' := exist _ (PS.add x s) _ in
22 match ofold left (fun v w ⇒ obind (dfs' s' w v) (fun v' ⇒ Some (exist _ v' _))) zs (Some v) with
23 | None ⇒ None
24 | Some v' ⇒ Some (exist2 _ _ (PS.add x v') _ _)
25 end
26 end
27 end
28 end.
29
30 Definition dfs (x : ident) (v : { v | visited PS.empty v })
31 : option { v' | visited PS.empty v' & (PS.In x v' ∧ PS.Subset v v' ) } :=
32 dfs' (exist _ PS.empty _)

<caption>FIGURE 19 – Algorithme de recherche en profondeur certifiant</caption>

on peut donc associer un graphe dans lequel chaque dépendance entre étiquettes du nœud est
reflétée par un arc. Si le graphe est acyclique, on dit que le nœud est causal, voir **définition 2**.

**Définition 2** (Nœud « causal »).

$$
\text{node\_causal } n := \exists V A, \text{AcyGraph } V A \land (\forall \alpha_x \alpha_y, \vdash n \mid \alpha_y \underset{\text{dep}}{\stackrel{\text{dep}}{\rightleftarrows}} \alpha_x \implies \alpha_x \to_A \alpha_y)
$$

4 Preuves par induction causale

Des travaux antérieurs [5, §2.3] présentent une approche permettant de construire un schéma d'induction pour les nœuds causaux. Dans la suite de cette section, on rappelle ce schéma avec plus de détails. On propose également un autre schéma d'induction basé sur UsedInst. On applique ensuite ces schémas pour prouver le déterminisme du modèle sémantique de Vélus.

4.1 Principe d'induction sur les étiquettes

Etant donné un graphe acyclique caractérisé par AcyGraph V A, on peut extraire un ordre
topologique des étiquettes, sur lequel on peut aisément raisonner par induction. La figure 20
présente les règles de construction de cet ordre. La liste vide représente un ordre valide. Pour
ajouter un sommet à la liste, il faut que (1) ce soit bien un sommet du graphe, (2) qu'il n'apparaisse pas dans la liste, et (3) que tous les prédécesseurs, transitivement, de ce sommet soient déjà dans la liste. Pour ce dernier critère, on a prouvé que ne prendre que les arcs immédiats $(\alpha_y \to_A \alpha_x)$ donne une formulation équivalente. Cela dit, on préfère utiliser la formulation de la figure 20, qui est plus simple à manipuler dans nos preuves car elle correspond mieux à celle d'AcyGraph. En particulier, on établit l'existence d'un ordre topologique sur l'ensemble des sommets de tout graphe acyclique, comme énoncé dans la figure 20.

$$ \frac{\text{TopoOrder (AcyGraph VA) } \text{lord} \qquad \alpha_x \in V}{\neg \ln \alpha_x \text{ lord} \quad (\forall \alpha_y, \alpha_y \to_A^+ \alpha_x \implies \ln \alpha_y \text{ lord})} \qquad \text{TopoOrder (AcyGraph VA) } (\alpha_x :: \text{lord}) \\ \text{TopoOrder (AcyGraph VA) } \llap{\boxed{\phantom{\frac{A}{A}}}\quad} \text{AcyGraph VA} \implies \exists \text{ lord}, (\forall \alpha_x, \alpha_x \in V \iff \ln \alpha_x \text{ lord}) \wedge \text{TopoOrder (AcyGraph VA) } \text{lord} $$

<caption>FIGURE 20 – Définition et existence d'un ordre topologique</caption>

Le principe d'induction est présenté en **lemme 1**. On pose $P\_var$: étiquette $\to$ Prop le prédicat à prouver pour chaque étiquette d'un nœud. La fonction **locals** collecte l'ensemble des étiquettes apparaissant dans les déclarations locales du bloc, y compris celles associées aux **last**. Le nœud doit être causal. Pour toute étiquette $\alpha_x$, si toutes les étiquettes dont $\alpha_x$ dépend respectent $P\_var$, alors $\alpha_x$ doit respecter $P\_var$. Si ces deux conditions sont respectées, alors on sait que toutes les étiquettes apparaissant dans les entrées, sorties et déclarations locales du nœud respectent $P\_var$.

**Lemme 1** (Induction sur les étiquettes d'un nœud causal).

$$ \begin{array}{l} \textbf{si} \quad \text{node\_causal} \text{ (node (ins) returns (outs) blk)} \\ \textbf{et} \quad (\forall \alpha_x, \ln \alpha_x (ins + outs + \text{locals blk}) \implies \\ \qquad (\forall \alpha_y, (ins + outs) \vdash blk | \alpha_x \stackrel{\text{dep}}{\leftarrow} \alpha_y \implies P\_var \alpha_y) \implies \\ \qquad P\_var \alpha_x) \\ \textbf{alors} \quad (\forall \alpha_x, \ln \alpha_x (ins + outs + \text{locals blk}) \implies P\_var \alpha_x) \end{array} $$

La preuve de ce lemme utilise **node\_causal** pour faire apparaître le graphe acyclique $g$ associé au nœud. On utilise le mécanisme d'induction habituel de Coq sur le témoin de **TopoOrder** associé à $g$ pour prouver que $P\_var$ est vraie, de proche en proche, pour chaque étiquette de l'ordre topologique. Pour une dépendance $\alpha_x \stackrel{\text{dep}}{\leftarrow} \alpha_y$ dans le nœud, il y a un arc de $\alpha_y$ vers $\alpha_x$ dans le graphe, donc $\alpha_y$ apparaît avant $\alpha_x$ dans l'ordre topologique, et donc, par induction, $P\_var \alpha_y$ est vrai.

## 4.2 Principe d'induction sur les expressions

L'élément syntaxique central induisant une dépendance est l'équation. Considérons l'équation $(x, y) = \text{es}$. Le flot associé à $x$ est le premier flot associé à es. Pour établir une propriété $P\_var$ sur ce flot, il faut d'abord raisonner par induction sur les expressions es. C'est l'objectif du deuxième schéma d'induction que l'on présente maintenant. On pose $P\_exp: \exp \to nat \to \text{Prop}$,
un prédicat sur le k-ième flot produit par une expression, et P_exps, un prédicat équivalent sur une liste d'expressions. Si toutes les variables utilisées instantanément du k-ième flot de l'expression e satisfont P_var, alors P_exp e k doit être satisfaite. Le schéma d'induction correspondant est présenté en **lemme 2**. Il suit la définition de UsedInst de la **section 3.1.1**.

**Lemme 2** (Induction sur UsedInst).

$$ si \ P\_var \ \alpha_x \implies P\_exp \ x \ 0 $$

$$ et \ \forall k, P\_exp \ e \ 0 \land P\_exps \ e_{s_0} \ k \land P\_exps \ e_{s_1} \ k \implies P\_exp \ (\textcolor{blue}{if} \ e \ \textcolor{blue}{then} \ e_{s_0} \ \textcolor{blue}{else} \ e_{s_1}) \ k $$

$$ et \ \forall k, P\_exps \ e_{s_0} \ k \implies P\_exp \ (e_{s_0} \ \textcolor{blue}{fby} \ e_{s_1}) \ k $$

et ...

$$ alors \ \forall e \ k, (\forall x, x \in \text{UsedInst}_\Gamma(e)[k] \implies P\_var \ x) \implies P\_exp \ e \ k $$

Pour chaque forme d'expression, l'utilisateur du schéma doit prouver que, si un ensemble d'hypothèses d'induction est vérifié, alors P_exp est vraie pour l'expression. Par exemple, dans le cas d'une variable, l'utilisateur doit prouver P_exp x 0, sous l'hypothèse que l'étiquette associée à x respecte P_var. Pour le **if-then-else**, on a une hypothèse pour la condition, et une pour chacun des deux opérandes. Le cas du **fby** est plus intéressant : conformément à la définition de UsedInst, on n'a qu'une hypothèse d'induction pour l'opérande de gauche. Quelque soit la propriété P_exp considérée, elle doit donc pouvoir être prouvée indépendemment de l'opérande de droite du **fby**. C'est le cas dans la preuve de déterminisme.

## 4.3 Application : déterminisme de la sémantique

On s'intéresse maintenant à la propriété de déterminisme du modèle sémantique, qui peut être exprimée comme « l'exécution d'un nœud pour une entrée donnée produit toujours la même sortie ». Cette propriété est formalisée par le **théorème 1**.

**Théorème 1** (Déterminisme de la sémantique).

$$ si \ \text{node\_causal} \ G(f) $$

$$ et \ G \vdash f(xs) \Downarrow ys_1 \quad et \ G \vdash f(xs) \Downarrow ys_2 $$

$$ alors \ ys_1 \equiv ys_2 $$

Ce théorème fait l'hypothèse de deux exécutions possibles du nœud. Cela signifie qu'il existe deux historiques distincts $H_1$ et $H_2$ qui satisfont les contraintes de ce nœud. Le but est de prouver qu'en réalité, ces historiques correspondent, pour chaque variable du nœud. Ce n'est vrai que pour les nœuds causaux. En effet, dans un nœud contenant la déclaration cyclique $x = x$, on peut associer n'importe quel flot à $x$.

Pour illustrer la structure générale de la preuve, on s'appuie sur le programme **after_n** présenté en **figure 21**. Ce programme renvoie **false** pendant n instants, puis **true**. Après cela, le compteur interne c n'est plus mis à jour pour éviter un dépassement d'entier négatif.

Dans ce programme, les valeurs de c et b à l'instant $n+1$ dépendent de leurs valeurs à l'instant $n$. Pour prouver que les flots associés à c et b dans $H_1$ et $H_2$ correspondent, on doit donc raisonner par induction sur $n$. L'induction doit être globale au nœud puisque la définition d'une variable peut dépendre de la valeur précédente de n'importe quelle autre : dans l'exemple, c dépend de la valeur précédente de b. On utilise la relation d'équivalence jusqu'à $n$ définie ci-dessous. Si on peut prouver $xs_1 \equiv_n xs_2$ pour un $n$ arbitraire, alors on peut prouver $xs_1 \equiv xs_2$.
node after_n(n : int) returns (b : bool)
var c : int;
let
c = n fby (if b then c else (c - 1));
b = c <= 0;
tel

<caption>FIGURE 21 - Programme after_n</caption>

**Définition 3** (Equivalence jusqu’à *n*).

$$xs \equiv_0 ys \qquad x \cdot xs \equiv_{n+1} y \cdot ys \quad \mathbf{ssi} \quad x = y \quad \mathbf{et} \quad xs \equiv_n ys$$

Le cas $n = 0$ de l'induction est trivial. Pour le cas inductif, on fait l'hypothèse que tous les flots de $H_1$ et $H_2$ sont égaux jusqu'à $n$, et on veut prouver qu'ils le sont toujours jusqu'à $n + 1$. La propriété qu'on veut prouver pour chaque étiquette $P\_var$ dépend donc du rang $n$, et des deux historiques $H_1$ et $H_2$. Elle dépend aussi d'un environnement $\Gamma$ pour faire le lien entre les noms des flots et leurs étiquettes. Cet environnement est déduit des déclarations des entrées, sorties, et variables locales du nœud. On définit donc

$$P\_var \alpha_x := \forall x, \Gamma(x) = \alpha_x \implies H_1(x) \equiv_{n+1} H_2(x)$$

La preuve procède par induction sur l'ordre topologique des variables, comme décrit dans le lemme 1. Dans l'exemple, $P\_var$ est immédiatement vraie pour $n$ qui est une entrée. On la prouve ensuite pour $c$ qui ne dépend instantanément que de $n$, puis pour $b$ qui dépend de $c$.

**Induction sur les expressions** Pour chaque étiquette, il y a dans le nœud une équation ($x_1, ..., x_m$) = es définissant le flot correspondant. Par la règle sémantique de l'équation, on sait que le flot associé à l'étiquette de $x_k$ est le $k$-ième flot produit par es. On montre donc le lemme ci-dessous qui indique que les $k$-ième flots produits correspondent jusqu'à $n + 1$. Pour le prouver, on utilise le principe d'induction du lemme 2.

**Lemme 3** (Equivalence jusqu'à $n + 1$ pour les expressions).

$$ 
\begin{array}{l@{\qquad}l}
\mathbf{si} & \forall x, H_1(x) \equiv_n H_2(x) \\
\mathbf{et} & \forall x \alpha_x, \alpha_x \in \text{UsedInst}_\Gamma(e)[k] \implies \Gamma(x) = \alpha_x \implies H_1(x) \equiv_{n+1} H_2(x) \\
\mathbf{et} & bs_1 \equiv_{n+1} bs_2 \\
\mathbf{et} & G, H_1, bs_1 \vdash e \Downarrow \mathbf{vss}_1 \quad \mathbf{et} \quad G, H_2, bs_2 \vdash e \Downarrow \mathbf{vss}_2 \\
\mathbf{alors} & \mathbf{vss}_1[k] \equiv_{n+1} \mathbf{vss}_2[k]
\end{array}
$$

Pour prouver ce résultat, il faut que les flots de $H_1$ et $H_2$ soient égaux jusqu'à $n$, ce qu'on sait par hypothèse d'induction. Il faut aussi que les flots associés aux variables utilisées instantanément pour le $k$-ième flot soient égaux jusqu'à $n + 1$. Cette différence vient du traitement de fby. Considérons l'équation $c = n$ fby (if b then c else (c - 1)) de l'exemple. Pour prouver que les flots associés à c sont égaux jusqu'à $n + 1$, il faut prouver que les flots associés à n le sont, puisque c en dépend instantanément. En revanche, on a seulement besoin de savoir que les flots associés aux variables à droites du fby sont égaux jusqu'à $n$, puisque leurs valeurs à l'instant $n + 1$ ne sont pas utilisées instantanément. Cette intuition est formalisée dans lemme 4, qui est prouvé par co-induction sur les définitions de fby et fby1.

**Lemme 4** (Equivalence jusqu'à $n + 1$ pour fby).

$$\mathbf{si} \quad xs_1 \equiv_{n+1} xs_2 \quad \mathbf{et} \quad ys_1 \equiv_n ys_2 \quad \mathbf{alors} \quad \text{fby } xs_1 \quad ys_1 \equiv_{n+1} \text{fby } xs_2 \quad ys_2$$
**Induction sur la sémantique des déclarations locales** Pour trouver l'équation définissant un flot, on procède par induction sur l'arbre de syntaxe des blocs. On rencontre une difficulté pour les flots déclarés localement, comme c dans l'exemple. En effet, la règle pour les déclarations locales de la figure 10 indique seulement qu'un historique interne existe et associe un flot à chaque déclaration interne, mais n'expose pas ces flots. Ainsi, la propriété P_var globale au nœud n'est pas suffisante pour traiter ces étiquettes locales.

Pour surmonter cette complication, on définit une version instrumentée de la sémantique des blocs. Elle met en parallèle les deux exécutions du bloc, en ajoutant localement des informations sur la correspondance des flots associés aux déclarations locales. Ces informations sont préservées pendant les inductions imbriquées sur *n* et sur l'ordre topologique.

$$
\begin{array}{l@{\hspace{3em}}l@{\hspace{3em}}l}
\forall x, x \in \text{dom}(H'_1) & \iff & x \in \text{locs} & \forall x, x \in \text{dom}(H'_2) & \iff & x \in \text{locs} \\
& & \forall x e, (\text{last } x = e) \in \text{locs} & \implies & G, H_1 + H'_1, bs \vdash \text{last } x = e \\
& & \forall x e, (\text{last } x = e) \in \text{locs} & \implies & G, H_2 + H'_2, bs \vdash \text{last } x = e \\
& & G, H_1 + H'_1, H_2 + H'_2, bs_1, bs_2 \vdash_{n,\text{lord}} \text{blks} & \forall x, x \in \text{locs} & \implies & H'_1(x) \equiv_n H'_2(x) \\
& & \forall x, \text{locs}(x) = \alpha & \implies & \alpha \in \text{lord} \implies & H'_1(x) \equiv_{n+1} H'_2(x) \\
& & \multicolumn{4}{c}{\text{let } G, H_1, H_2, bs_1, bs_2 \vdash_{n,\text{lord}} \text{var } \text{locs} \text{ let } \text{blks } \text{tel}}
\end{array}
$$

<caption>FIGURE 22 – Sémantique instrumentée, cas de la déclaration locale (cf. figure 10)</caption>

On note le jugement instrumenté *G*, *H*₁, *H*₂, *bs*₁, *bs*₂, ⊢*n,lord* *blk*. La règle pour les déclarations locales est donnée en figure 22. Elle suit la règle de sémantique donnée plus tôt pour les déclarations locales. Les deux dernières prémisses établissent la correspondance entre les deux exécutions. La prémisse ∀x, x ∈ *locs* ⇒ *H*′₁(*x*) ≡ₙ *H*′₂(*x*) impose que tous les flots locaux soient égaux jusqu'à *n*. Cela correspond à notre invariant d'induction sur *n*. De plus, la prémisse ∀x, *locs*(*x*) = α ⇒ α ∈ *lord* ⇒ *H*′₁(*x*) ≡ₙ₁ *H*′₂(*x*) impose que les flots associés aux étiquettes de *lord* soient égaux jusqu'à *n* + 1. Cette liste *lord* est un préfixe de l'ordre topologique manipulé par le principe d'induction du lemme 1. Cela correspond donc à notre invariant d'induction sur l'ordre topologique.

La structure de la preuve du théorème 1, en prenant en compte le modèle sémantique instrumenté, est la suivante : On procède par induction sur *n*. Par hypothèse d'induction, on sait que tous les flots du nœud sont égaux au rang *n*. On sait donc en particulier que tous les flots locaux le sont, mais on ne sait pas encore qu'ils sont égaux jusqu'à *n* + 1. On pose *lord* = [], la liste (vide) des étiquettes pour lesquelles on sait que les flots sont égaux jusqu'à *n* + 1, et on a donc *G*, *H*₁, *H*₂, *bs*₁, *bs*₂, ⊢*n,[]* *blk*. On utilise alors le principe d'induction du lemme 1 pour prouver que les flots associés à chaque étiquette du nœud sont égaux jusqu'à *n* + 1. Pour chaque étiquette *α*, on trouve l'équation définissant le flot correspondant et on utilise le lemme 3 comme décrit plus haut. Si l'étiquette est celle d'une déclaration locale, on ajoute *α* à la liste *lord*, et on obtient *G*, *H*₁, *H*₂, *bs*₁, *bs*₂, ⊢*n,α::lord* *blk*. À la fin de l'induction, on a *G*, *H*₁, *H*₂, *bs*₁, *bs*₂, ⊢*n,(locals *blk*)* *blk*. Autrement dit, on sait que tous les flots locaux sont égaux jusqu'à *n* + 1, parce qu'ils sont tous dans la liste. C'est équivalent à incrémenter *n*, et vider la liste, comme énoncé formellement dans le lemme 5, ce qui termine la preuve.

**Lemme 5** (Sémantique instrumentée, passage de *n* à *n* + 1).

si $G, H_1, H_2, bs_1, bs_2, \vdash_{n,(locals blk)} blk$ alors $G, H_1, H_2, bs_1, bs_2 \vdash_{n+1,[]} blk$
# 5 Conclusion

Dans cet article, nous avons décrit l'ajout de deux nouvelles structures d'activation dans Vélus : le *switch* et les déclarations locales. Nous avons aussi ajouté à Vélus des variables partagées au moyen de l'opérateur *last*. Nous avons modélisé la sémantique à flot de données de ces structures. Les nouvelles règles sémantiques s'intègrent modulairement au modèle de Vélus, c'est-à-dire sans modifier les règles existantes. Nous avons aussi adapté l'analyse de dépendance de Vélus pour traiter ces nouvelles constructions. Nous avons présenté en détail un algorithme d'analyse de graphe générant un témoin de l'absence de cycle dans le graphe de dépendance d'un nœud. Enfin, nous avons défini un principe d'induction tirant parti de cette analyse.

**Travaux connexes** Les auteurs de [7] proposent une sémantique par réaction pour un language synchrone à flots de données avec structures d'activation. Dans [8], la sémantique des structures d'activation est donnée « par traduction » dans le langage noyau. De la même manière, notre règle pour le *switch* est définie en fonction de l'opérateur d'échantillonage *when*, qui est aussi utilisé lors de sa compilation. Ces articles formalisent également la sémantique et la compilation de machines à états hiérarchiques dans un langage synchrone à flots de données. Nous travaillons actuellement à l'ajout de cette construction au compilateur Vélus. Du point de vue de l'analyse de dépendance, elle ne pose à priori pas plus de difficultés que les *switch*. Sa sémantique est en revanche plus difficile à exprimer dans notre modèle relationnel à flots de données.

Notre implémentation de l'algorithme de recherche en profondeur a suivi, sans le savoir, le travail de F. Pottier. Il note [15, §4] que son algorithme, comme le notre, utilise sur la pile d'appel un espace proportionnel à la profondeur maximale de recherche, et qu'une implémentation en style récursif terminal avec pile explicite éviterait ce problème. Dans notre cas les graphes manipulés sont issu de programmes écrits par l'utilisateur et il y a donc peu de chance d'arriver à un débordement de la pile. Comme dans ce travail on utilise des types dépendants pour justifier la terminaison de l'algorithme, mais contrairement à lui on utilise la bibliothèque *Program* de M. Sozeau [19] pour éviter de programmer avec des tactiques.

**Discussion** Dans notre développement Coq, les règles sémantiques de Vélus présentées dans cet article sont encodées par des prédicats inductifs. Manipuler cet encodage dans un script de preuve Coq est commode, puisqu'on peut raisonner par introduction, inversion et induction. Entre autres, la preuve de correction des algorithmes de compilation pour ces structures, qui n'a pas été présentée dans cet article, est relativement directe.

Le principe d'induction sur un nœud causal présenté dans cet article est une idée centrale pour le langage. Si, dans cet article, nous ne l'avons appliqué qu'à la preuve du déterminisme du modèle sémantique, il nous a été utile pour établir d'autres propriétés. Prouver la correction du système d'horloge, c'est-à-dire l'adéquation du rythme des flots produits aux annotations statiques d'horloges, nécessite par exemple l'utilisation de ce principe. Cette propriété est indispensable pour démontrer la correction du compilateur.

**Remerciements** Nous remercions L. Brun pour ses contributions à Vélus, et en particulier son travail sur l'intégration des types énumérés, sans lesquels l'ajout de *switch* n'aurait pas été possible. Nous remercions également nos rapporteurs pour leurs remarques qui ont permis d'améliorer le contenu de cet article. Ce travail a été soutenu par le projet ANR JCJC FidelR 19-CE25-0014-01 « Fidelity in Reactive Systems Design and Compilation ».
Bibliographie

[1] Albert BENVENISTE, Timothy BOURKE, Benoit CAILLAUD, Bruno PAGANO et Marc POUZET : A type-based analysis of causality loops in hybrid modelers. In *Proceedings of the 17th International Conference on Hybrid Systems : Computation and Control (HSCC 2014)*, pages 71–82, Berlin, Allemagne, avril 2014. ACM Press.

[2] Dariusz BIERNACKI, Jean-Louis COLAÇO, Gregoire HAMON et Marc POUZET : Clock-directed modular code generation for synchronous data-flow languages. In *Proceedings of the 9th ACM SIGPLAN Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2008)*, pages 121–130, Tucson, AZ, États-Unis, juin 2008. ACM Press.

[3] Timothy BOURKE, Lélio BRUN, Pierre-Évariste DAGAND, Xavier LEROY, Marc POUZET et Lionel RIEG : A formally verified compiler for Lustre. In *Proceedings of the 2017 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)*, pages 586–601, Barcelone, Espagne, juin 2017. ACM Press.

[4] Timothy BOURKE, Lélio BRUN et Marc POUZET : Mechanized semantics and verified compilation for a dataflow synchronous language with reset. In *Proceedings of the 4(POPL):1–29, janvier 2020*.

[5] Timothy BOURKE, Paul JEANMAIRE, Basile PESIN et Marc POUZET : Verified Lustre normalization with node subsampling. *ACM Transactions on Embedded Computing Systems*, 20(5s):Article 98, octobre 2021.

[6] Paul CASPI, Daniel PILAUD, Nicolas HALBWACHS et John A. PLAICE : LUSTRE : A declarative language for programming synchronous systems. In *Proceedings of the 14th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1987)*, pages 178–188, Munich, Allemagne, janvier 1987. ACM Press.

[7] Jean-Louis COLAÇO, Grégoire HAMON et Marc POUZET : Mixing signals and modes in synchronous data-flow systems. In *Proceedings of the 6th ACM International Conference on Embedded Software (EMSOFT 2006)*, pages 73–82, Séoul, Corée du Sud, octobre 2006. ACM Press.

[8] Jean-Louis COLAÇO, Bruno PAGANO et Marc POUZET : A conservative extension of synchronous data-flow with state machines. In *Proceedings of the 5th ACM International Conference on Embedded Software (EMSOFT 2005)*, pages 173–182, Jersey City, États-Unis, septembre 2005. ACM Press.

[9] Jean-Louis COLAÇO, Bruno PAGANO et Marc POUZET : Scade 6 : A formal language for embedded critical software development. In *Proceedings of the 11th International Symposium on Theoretical Aspects of Software Engineering (TASE 2017)*, pages 4–15, Nice, France, septembre 2017. IEEE Computer Society.

[10] Jean-Louis COLAÇO et Marc POUZET : Clocks as first class abstract types. In *Proceedings of the 3rd International Conference on Embedded Software (EMSOFT 2003)*, volume 2855 de Lecture Notes in Ele ctrical Engineering, pages 134–155, Philadel phie, PA, États-Unis, octobre 2003. Springer.

[11] COQ DEVELOPMENT TEAM : *The Coq proof assistant reference manual*. Inria, 2020.

[12] Pascal CUOQ et Marc POUZET : Modular causality in a synchronous stream language. In *10th European Symposium on Programming (ESOP 2001), part of European Joint Conferences on Theory and Practice of Software (ETAPS 2001)*, volume 2028 de Lecture Notes in Ele ctrical Engineering, pages 237–251, Gènes, Italie, avril 2001. Springer.

[13] Xavier LEROY : Formal verification of a realistic compiler. *Comm. ACM*, 52(7):107–115, 2009.

[14] Roberto LUBLINERMAN, Christian SZEGEDY et Stavros TRIPAKIS : Modular code generation from synchronous block diagrams : Modularity vs. code size. In *Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2009)*, pages 78–89, Savannah, GA, États-Unis, janvier 2009. ACM Press.

[15] François POTTIER : Depth-first search and strong connectivity in Coq. In *Journées Francophones des Langages Applicatifs (JFLA)*, janvier 2015.
[16] Marc POUZET : *Lucid Synchrone, version 3. Tutorial and reference manual*. Université Paris-Sud, avril 2006.

[17] Marc POUZET : ZRun. https://github.com/marcpouzet/zrun/blob/master/src/coiteration.ml, 2021.

[18] Marc POUZET et Pascal RAYMOND : Modular static scheduling of synchronous data-flow networks : An efficient symbolic representation. In *Proceedings of the 9th ACM International Conference on Embedded Software (EMSOFT 2009)*, pages 215-224, Grenoble, France, octobre 2009. ACM Press.

[19] Matthieu SOZEAU : Subset Coercions in Coq. *Lecture Notes in Computer Science*, (4502):237-252, 2007.
# Formal proofs applied to system models.

Évelyne Contejean, Andrei Samokish

LMF – Université Paris-Saclay, CNRS, ENS Paris-Saclay

## Abstract

Usually, the description of nuclear equipment by the FMEA (Failure Mode and Effects Analysis) method can be of considerable length (up to 5,000 lines); on the other hand, the number of rules used for the verification of this equipment is small. In addition, upstream, there is the question of trust in the tools that generate these descriptions for complex equipment, that is to say, made up of several thousand objects (requirements, functions, interfaces, behaviors).

Our objective is to formally prove in the Coq proof assistant the accuracy and exhaustiveness of the safety analysis for these nuclear equipments, by proposing a more modular and more abstract framework which is based on an axiomatic description of the systems. - these axioms being either accepted or proven independently of the verification itself. The very nature of the inductive types of Coq is perfectly suited to the description of complex systems, which are systems of systems in interaction. We have a first prototype that demonstrates the feasibility of this approach, for simple properties which are effectively proven by reflection - for example, the study of flows, which must first be produced and then consumed exactly once in the whole system.

We open the way to a general approach for the proofs of the properties of a (model of) systems and study the kind of properties that can be demonstrated in this way. Finally, we propose the approach for faithful translation of a DSL (domain-specific language) tool into Coq and the proof of its correctness.

## 1 Motivation

For about 15 years, the idea that systems can be modeled has been developing, and more and more processes, including safety and security analysis, have started to be backed by models. Such models can be used to perform simulations but may also reduce complexity and turn complex problems into smaller ones from a logical point of view. This is the case for Failure Mode and Effect Analysis (FMEA), where the risk analysis of a complex system is turned into an extensive list of risk reduction means for each couple of functions and components in the system. More generally, for complex systems, the safety case becomes a complicated document or set of information that transforms a high-level goal into a huge number of much simpler goals. An FMEA for a Nuclear Steam Generator (used as an example in this paper) is in the order of magnitude of thousands of lines.

The idea that software tools can help handle this complexity has been in the air for a long time. However, software tools are complex systems that can be challenged as well as any other complex software. When dealing with complex system models, the question of how confident we can be in the tools to handle all situations and faithfully describe the system of interest is at stake. In the software domain, Formal Methods (FM) are already used to verify that complex software performs correctly (see proof of C compiler by X. Leroy [10]), so it seems interesting
to investigate a similar approach for systems models and related tools.

We notice that the general definition of a system is inductive: broadly speaking, systems are made of (sub)systems in interactions, so when trying to prove some property on a system, it is logical to deduce that property from some properties of its subsystems. More generally, systems engineering is mainly built upon inductive breakdown structures: Relation Block Diagram (RBS), Functional Block Diagram (FBS), Project breakdown structure (PBS)... Classical safety methods, although inductive or deductive, are also based on the inductive design of systems. For this reason, we decided to investigate inductive types as a foundation for the formal definition of a system.

With this objective in mind, we should take care of two critical issues:

First, FMs are usually applied to detailed system behavior. Using FM methods seems very useful when the logic of the system is already defined. For example, formal Event-B specifications applied to FMEA give interesting results [5]. However, the later a problem is discovered, the more expensive the solution [11], so it is relevant to investigate the use of FM at the specification level, especially when high-level performance or non-functional requirements are refined into lower-level requirements. The development of Model-Based Systems Engineering provides an opportunity here because these tools and methods keep track of the refinement of the system design from the external analysis to the detailed component description. This objective is upstream w.r.t. the usual application of FM

Second, there can be significant drawbacks in FM application (a detailed description of problems can be found in [4]):

* FMs are difficult to learn and apply. Many assurance practitioners perceive the usage of FMs as negative.

* The number of practical (comparative) case studies using preliminary initial system design FMs is still too low to draw valuable and firm conclusions on FM effectiveness.

* FMs have been suffering from fragile effectiveness and productivity in the context where some physical processes are supposed to be controlled with a computer system.

* The effectiveness of formal models can be significantly reduced because of uncontrollable gaps between models and their implementations.

So, we need to provide an intermediate step between the FM-proof assistant and the system and safety model. The complexity of FM needs to be hidden from the end-user, and at the same time, it shall apply efficiently. For this reason, we propose a DSL (domain-specific language) as a front-end user interface that will be accessible to the engineer without knowledge of FM.

Our approach intends to make a bridge between system model description and formal systems, simplifying the dialog between engineers and mathematicians and allowing them to investigate system models with FM in the initial design stages.
## 2 Process and vocabulary

Fig. 1. Explains the different transformations that allow translating a system model faithfully into a Proof assistant program. In this section, we introduce both the process and the vocabulary corresponding to each translation step.

<figure><img src="image_65.png" /><figcaption>Fig. 1. Model formalization process</figcaption></figure>

1. At the very beginning, Systems engineers describe systems through *System item, system interactions* (flows), *system artifacts* (used to describe, specify, and communicate about the system) (see INCOSE handbook [13]) - *artifacts* includes requirements, functions, flows, components, systems (in the meaning combination of functions and components). For systems, we may differentiate artifact categories or types from artifact instances. An artifact category may be ‘function’ while an artifact instance of “function” would be ‘function for heat transfer between primary and secondary circuit’.

2. Modeling the System of Interest is getting a standard way for specifying. During model formalization, engineers describe system *Artifacts* representing parts of the system of interest. Artifact instances are usually called objects, and Artifact categories are Object Types. Examples of model languages are UML, SysML, Domain Specific Languages (DSL)...Although some of these formalisms used to be partly diagram based, there is currently an effort to provide them with a complete syntactic definition.

3. Definition of Domain Specific Language (DSL) is a particular kind of model. At this step, we do use two main notions:
   * DSL types model artifacts categories
   * DSL terms model artifact instance and get a DSL type (i.e., DSL term ‘Steam Generator’ of DSL type ‘System’). In our process, we will consider a particular DSL that is simple enough to ease translation into a theorem prover and powerful enough to capture systems complexity.
   If we first define a model, we need to translate it into our DSL. The translation will associate to an object a DSL term and to an object type a DSL type.

4. The next step is the translation of the DSL into COQ.
   In COQ also, we can distinguish between terms and types.
   In the paper, we show it’s possible to translate the DSL types into a single Inductive Type that we will name COQ_DSL. COQ_DSL is, in fact, a mutually inductive type, and each mutually defined inductive type in COQ_DSL corresponds to a single DSL type. So it’s possible to make a one-to-one correspondence between DSL types and some COQ types.
   Once this is done, DSL terms can also be translated into COQ terms (see Fig.2).
   At this step, the System Model is defined as a set of artifacts with DSL types assigned and translated to COQ terms with appropriate inductive type constructors.
<figure><img src="image_66.png" /><figcaption>Fig. 2. Commutativity diagram between DSL and COQ terms</figcaption></figure>

5. Finally, we can specify and prove the properties of the system and its artifact. The main task at this step is to translate system and model properties and rules into COQ theorems and prove them.

## 3 Model example

<figure><img src="image_67.png" /><figcaption>Fig. 3. Nuclear plant principle</figcaption></figure>

<figure><img src="image_68.png" /><figcaption>Fig. 4. Steam generator preliminary design</figcaption></figure>

As example of a system model to be described, we took the general Nuclear Steam Generator (fig. 3,4) description represented in the AFCEN* guide [12]. Steam generators are heat exchangers used to make steam from water with the heat produced in a nuclear reactor core and are used in pressurized water reactors between the primary and secondary coolant loops. This is a good example of a system with a lot of safety requirements, a lot of physical relations between components, and some functional data flow between them. We will introduce DSL (Domain Specific Language) to describe the Generator model and then translate it into a formal description.

<footnote>* AFCEN - French Association for Design, Construction and In-Service Inspection Rules for Nuclear Steam Supply System Components</footnote>
In describing this example, we need to select the formal syntax for denoting system items and their hierarchical relationships and the formal syntax for denoting relations between system items. We can then introduce some inductive breakdown structure denoting the system as a whole. In our particular example, we introduce several Object Types like ‘System’, ‘Components’, ‘Function’, ‘Requirement’, and several categories for flows/relationships between these Objects Types: ‘Data flow’, ‘Physical flow’, and ‘Refine’. Some system logic terms are also defined: ‘System’ can contain objects of ‘Component’ only, ‘Component’ can contain ‘Component’ or ‘Function’, and so on... In fig.5, we provide a simplified model implemented with the given Object Types above. ‘Steam Generator Boiler’ of type ‘System’ is our system of interest; this object contains children object of type ‘Component’ exchanging flows of type ‘Physical flow’. The example presented is simplified; it has only several objects on the diagram. Our real example is based on a Use Case in the AFCEN guide [12] for risk analysis of nuclear pressurized equipment and consists of 66 Components, 153 Functions, 160 Physical flows, and 495 Requirements.

<figure><img src="image_69.png" /><figcaption>Fig. 5. Simplified model of Nuclear Steam Generator</figcaption></figure>

## 4 Domain-Specific Language

Now we introduce the DSL supporting the syntactic description of our system through its hierarchy of objects as shown in Fig.5. Each object in the system model has a type, and hierarchical relations between types are strictly defined (some types can be recursive, e.g., a system may be composed of components and components may be composed of components). We propose interpreting these relations between DSL types as a Regular language (generated by type-3 grammar in Chomsky hierarchy [14]). I.e., if we have such a hierarchy of DSL terms: ‘system 1’ → ‘function A’ → ‘requirement X’, which barely denotes that requirement X is allocated to function A that is allocated to the system, then an appropriate list of types for the
‘requirement X’ position in the hierarchy will be [system] — [function] — [requirement] and it is an accepted word for the language. Regular Grammar and Finite Automata(FA) being equivalent [1], we propose to describe our DSL language with the FA ($\Sigma$, S, s0, $\delta$, F) such that:

* $\Sigma$ – list of input alphabet = list of DSL types,

* S is a set of states (one state per DSL type),

* s0 – initial state (represents the root of objects DSL types hierarchy),

* $\delta$ is the state-transition function (displayed graphically in fig.6),

* F is the set of final states, equal to S to represent the simple DSL (hierarchical description in our example can be stopped at any level)

<figure><img src="image_70.png" /><figcaption>**Fig. 6. Finite automata presentation of DSL types**</figcaption></figure>

Our sample DSL here is not universal. There can be other DSLs based on different types of grammar, some specific restrictions can be applied (like the rule ‘each Component should contain a function), and so on. But most systems can be defined with such a simple breakdown. Note that DSL represented in Fig.6 is a type relation diagram, so having an arrow means that in a concrete example, there can be several children object instances for the given type (possibly no children).

At this step, our system of interest could be modeled either directly in a tool supporting the DSL in Fig 6 faithfully or by translating from an existing MBSE tool into our DSL. Our objective is to start from a DSL that is simple enough to enable a faithful translation into a theorem prover but smart enough to capture the complexity of a system model. The power of our approach relies on this trade-off between simplicity and faithfulness.

# 5 DSL model Translation

We show now that our DSL can be translated to an inductive type [8] which is a well-founded logical concept preserving the original semantics of DSL. It is possible to find a theorem prover supporting Inductive Types. We decided to use the well-known proof assistant COQ[6], based on the Calculus of Inductive Constructions (CIC). To reach our goal, we need to translate our DSL faithfully into COQ (according to Fig.2 in section 2), to define a list of formal rules that a system description in the DSL should comply with, and prove them with COQ tactics.
First, we define an inductive type "Direction" with possible values 'input' and 'output' to encode the direction of functional or requirement data flow messages. "direction" will be useful for any translation of DSL terms denoting messages or interactions between system items.

Inductive direction : Set := input | output.

Next, DSL types are translated into COQ types in a one-to-one manner, and these COQ types will be defined as a mutually inductive type that we call COQ_DSL. As an inductive type, each COQ type is built with a set of constructors.

Consider the DSL type 'system'; the first constructor CSystem in Coq allows creating new COQ terms of type 'system'. Then CComponent_System allows aggregating a set COQ_DSL 'components' to a COQ_DSL 'system'. CFunction_System allows aggregating 'functions' in a 'system' and CSystem_System allows adding a set of terms of type 'system' in a 'system' (fig. 7). The constructors mimic the way we can build systems with the DSL and translate them into COQ.

With this translation specification in mind, we developed an automated generation of the type system in Coq based on a DSL with a one-to-one translation of DSL types into COQ types. Below you will find a pseudo-code example for translating a DSL into a COQ script file. Assume that all DSL types exist as a list in the typeCollection, and we have functions to get a list of children DSL types and to understand if the relation describes some interface (flow).

This way, the definition of DSL described in the first part of the paper can be translated into an inductive types in COQ, as presented in Fig. 7. On the image, you can see the top DSL type 'System', with all related DSL types reminded regarding each type in COQ (see fig.6 for DSL type relations). The 'with' keyword in the script remind all types are mutually inductive. We use natural numbers to encode unique identifiers assigned to each type, this is done to support the ability to distinguish objects instances. Object attributes describing some properties can be assigned similarly; a small example of properties will be shown in the next section.

<figure><img src="image_71.png" /><figcaption>Fig. 7. Translation DSL into COQ inductive types</figcaption></figure>
# 6 Translation of system model to COQ

Having defined the translation of DSL types into COQ types, we now address the translation of DSL terms into COQ terms. We do use a recursive bottom-up algorithm starting from leaf DSL items and then translating upper DSL items with the set of children COQ terms already translated. After translation, we do compile the resulting files into a COQ module. This step is already a proof of correctness of the export process because COQ will warn if any inconsistency is found between translated DSL terms and types.

In the example given (fig.8), you can see the part of the hierarchy of objects and the flow input (the real example of this system contains more than 1000 lines in a COQ file):

* `Steam_Generator_Boiler` is an object of type `System`, is a parent of several Components: `Drying_block`, `Feedwater_inlet`, `Water_tank` (and some others in real code)

* `Drying_block` in an object of type `component`, it has some children of type `Function` and some children of type `Component`

* `Feedwater_inlet` is also an object of type `Component`, consuming 'Secondary_water' flow of type 'Physical flow.'

```
...
Definition Feedwater_inlet_27 := CFunction Component [ ... ]
  (CPhysical_flow Component [ Secondary_water; ... ] input
   (CComponent 2194728288258))).
...
Definition Drying_block_11 := CFunction Component [ ... ]
  (CComponent Component [ ... ]
   (CComponent 1103806595096)).
...
Definition Steam_Generator_Boiler_1 := CComponent System
  [ Drying_block_11;
    Feedwater_inlet_27;
    Water_tank_32;
    ... ]
  (CSystem 1013612281857).
```

<caption>**Fig. 8.** shortened representation of data model in the COQ</caption>

The following pseudo python code is intended to walk through all objects of DSL types and generate appropriate commands into the COQ script resulting in the definition of the system with Coq inductive type:

```
Walk recursively through hierarchical object structure:
When all children are parsed:
  Write 'Definition ' + object name + ':='
For each child type:
  Write Child Type list Constructor +
```
List of children of the given type
Write Object Type constructor + object Identifier
Write '.'

To check that translation of the system model is robust, we did define a backward-
translation automatic script, converting COQ types into DSL and creating a DSL terms model
according to COQ data. To make a fair transition, this script calls COQ to load modules
containing data and reads defined type contents with COQ 'Print' command. It allows us to
compare initial and resulting data in the system definition tool we use to show that all
translations are bijective.

7 Verification

Once our system description is translated into COQ, we benefit from the advantages of a
theorem prover. We can formalize properties that should be met by the system, hypotheses and
demonstrate these properties.

For example, let's consider a property about data flows between Systems, Components, and Functions. An expected property of flows in the data model is that each produced flow should be consumed somewhere and conversely in the hierarchy of instances. Let's determine how to translate this property into COQ and make the proof that the model satisfies this property. We need to define the predicate as "any consumed data is produced" ("any produced data is consumed" is defined in the same way). Before specifying the goal, we need to create some recursive functions, walk through the hierarchy and look for flow objects. Here is the automatically created set of functions required for performing the verification (we display only a part of the proof).

"msgfunction" holds for a data d, a function g, and a production 'direction' (introduced in section 5) p if g contains (possibly in its subparts) the data flow d with direction p. Other definitions play a similar role for described COQ types. They study the given COQ type according to its definition and call appropriate functions recursively (to answer if the given flow with its direction is found in the term hierarchy or not):

Fixpoint msgfunction (d:Physical_flow) (p:direction) (g:Function): Prop :=
match g with
| CFunctionMM n => False
| CPhysical_flow_Function listData prod obj => (In d listData) /\ (prod = p) \
... 
end.
Fixpoint msgComponent (d:Physical_flow) (p:direction) (g:Component) {struct g}: Prop :=..
match g with
| CComponent n => False
| CFunctionissempath lf s => ( fold_left or (map (msgFunction d p) lf ) False ) \
... 
end.
Fixpoint msgsystem (d:Physical_flow) (p:direction) (g:System) {struct g}: Prop :=..
match g with
| CSystemMM n => False
| CComponentSystemMM lf s => ( fold_left or (map (msgComponent d p) lf ) False ) \
... 
end.

Finally, we can describe the goal, a property that can be proved by Coq tactics. Normally
the definition and Goal below should be understandable intuitively from the previous
definitions.

Definition EveryConsumedDataIsProduced (s: System) :=
forall (d:Physical_flow), (msgsystem d input s)-> (msgsystem d output s).

Goal (EveryConsumedDataIsProduced Steam_Generator_Boiler_1).
intro. simpl. tauto..
Qed.

Definition EveryProducedDataIsConsumed (s: System) :=
forall (d:Physical_flow), (msgsystem d output s)-> (msgsystem d input s).

With our experiments, we found that if the model is correct, it can be proved by Coq with
simple tactics (automatically, as the set of tactics required is trivial), in case of missed producer/
consumer COQ will simply warn about the failed theorem proof. In that case, we need to
perform some investigation to pinpoint the exact problem in the model. To find the problem,
we wrote a script for an ‘interactive’ search for the problem in COQ terms, calling some COQ
commands to perform checks and generating the next request with defined patterns.

8 FMEA

One interesting application of proofs of correctness and completeness is the safety (hazard)
analyses. There are several hazard analysis methods available for investigating possible failures
and describing ways to reduce risks. The most known ones are Failure Mode and Effect
Analysis [3] and System Theoretic Process Analysis (STPA). The FMEA safety analysis
method uses a physical component diagram (splitting the investigated system into parts, starting
from low-level components and proceeding up to the failure effect of the overall system). At
the same time, SPTA is based on a functional control diagram, analyzing the dynamic behavior
of the system [2]. FMEA is an inductive procedure summarizing upward effects on the system
from subsystems. So, the FMEA analysis is very well-structured, allowing to use of some
taxonomy to define the order of analysis actions and relations between them. A good example
of detailed taxonomy and conditions to be verified can be found in [7].

The DSL proposed in the first part of the paper is designed to describe the hierarchical
decomposition of a system into basic elements, which is the source for FMEA analysis. In the
image below, you can see the standard FMEA table according to (AFCEN guide [12]) with
some assigned DSL types for objects (with some properties added), representing data for
columns. The table (fig.9) is generated according to hierarchical object data stored in the system
model.
<figure><img src="image_72.png" /><figcaption>Fig. 9. FMEA tale with DSL language types assigned</figcaption></figure>

Having the data structure required and FMEA logic, we can define some completeness formal rules to prove in COQ. As an example of property defined by law, we consider the classification of equipment parts (depending on their role with regards to pressure resistance) defined by Autorité de sûreté nucléaire (Nuclear Safety Authority, ASN), represented in fig.10 (shortened comparing to [9]):

<figure><img src="image_73.png" /><figcaption>Fig. 10. Component classification logic</figcaption></figure>

To represent those properties in our model, we need first to define appropriate attributes for each Component object (with a defined list of possible values for each attribute):

* 'is used to pick up loads due to the pressure' – yes/no,

* 'is contributing to pressure resistance' – yes/no,

* 'is direct or indirect aggressive role' – yes/no,

* 'classification' – PP/AP/APCRP/APSRP.

Then those attribute values can be translated to the coq model as several sets and assigned
to object instances:

Inductive PressureLoads : Set := P_yes | P_no..
Inductive PressureResistance : Set := R_yes | R_no..
Inductive DirectAggressiveRole : Set := A_yes | A_no..
Inductive ObjType : Set := APCRP | PP | APSRP | AP..
Inductive Component : Type :=
  | CComponent : nat -> PressureLoads -> PressureResistance
  -> DirectAggressiveRole -> ObjType -> Component
  | CFunctionissemulation : list Function -> Component -> Component.
Definition Component3 := CComponent 3 P_no R_no A_yes AP.

From a practical point of view, identifying all pressure parts requires identifying parts that have an interface with primary or secondary circuits water and steam. So starting from a specification of all systems and parts interfaces, it is possible to formally identify all PP parts from the Coq Model. Explaining this in detail goes beyond the objective of this paper, but this is a good example of a part of the safety case that could be supported automatically and faithfully by a proof system. Of course, the identification of interfaces is based on systems engineer analysis and may be the weak spot of the proof.

9 Conclusion

The paper shows how system models can be translated into COQ definitions. Making proofs using only system descriptions allows us to work on a high abstract level (without detailed system behavior descriptions). This is especially major for investigating the correctness and completeness of the system with bottom-up safety analysis like FMEA.

Using a general system definition language (DSL) including recursive types definition, we did turn the DSL into a COQ inductive types; having this, we can translate the syntax of the system model (DSL terms) into definitions of COQ terms. Starting from system properties to be proven, we can translate them formally into COQ theorems and prove them either automatically or not. COQ is also capable of finding counterexamples in many cases if a property is not true (a small description is given at the end of section 7).

With this approach, systems and safety engineers get the possibility to back their systems
and safety analysis with formal proofs of correctness and completeness that have to be stated
in parallel.

Now we plan to investigate further topics to push the limits on this approach - investigate the completeness and correctness properties that systems and safety analysis should comply with. We started with simple properties in this paper, but generally, the Safety case comprises high-level goals that are decomposed into simpler elementary goals and action plans. We will investigate the formal rules behind such a decomposition. In parallel, we will look for a formal analysis regarding the completeness and correctness of a system design.

Then we need to check the resilience of a proof system like Coq when investigating models
made of 10th or 100th thousands of objects, as this is the size of the complex system models
we discuss.
After that, we would like to investigate the user's assistance when performing a system or safety analysis. For instance, in case we already know the functional and system architecture of the system, we can check for completeness and correctness properties and raise anomalies to the user. In case a safety goal is being decomposed, we can identify automatically if all subgoals are covering all the possibilities or not.

Finally, we will investigate how to connect MBSE tools to our system and safety formal DSL description, allowing the formal models to be filled by an existing modeler. Of course, we will have to prove that the translation is faithful, which could be made by bi-directional translation between the MBSE and the formal DSL and proof of evidence that there is a bijection.

## References

[1] Grune, D., Jacobs, C.J.H. (2008). Regular Grammars and Finite-State Automata. In: Parsing Techniques. Monographs in Computer Science. Springer, New York

[2] Sulaman, S., Beer, A., Felderer, M. et al. Comparison of the FMEA and STPA safety analysis methods—a case study. Software Qual J 27, 349–387 (2019).

[3] N. Storey, "Safety-critical computer systems", Addison-Wesley, 1996.

[4] Gleirscher M, Foster S, Woodcock J (2019) New opportunities for integrated formal methods. ACM Comput Surv 52 (6):117:1–117:36.

[5] I. Lopatkin, Y. Prokhorova, E. Troubitsyna, A. Iliasov, and A. Romanovsky. Patterns for Representing FMEA in Formal Specification of Control Systems. TUCS Technical Report 1003, 2011.

[6] COQ, https://coq.inria.fr/documentation, last accessed 2022/03/29.

[7] E. Pilugin, S. Authén, J-E. Holmberg. Proposal for the Taxonomy of Failure Modes of Digital System Hardware for PSA. 11th International Probabilistic Safety Assessment and Management Conference & The Annual European Safety and Reliability Conference At: Helsinki, 2012

[8] Pfenning, F., Paulin-Mohring, C. (1990). Inductively defined types in the Calculus of Constructions. In: Main, M., Melton, A., Mislove, M., Schmidt, D. (eds) Mathematical Foundations of Programming Semantics. MFPS 1989.

[9] Conformity assessment of nuclear pressure equipment. Autorite de surite nucleare. Guide N8. 2012.

[10] S. Blazy, Z. Dargaye, and X. Leroy. Formal verification of a C compiler front-end. In FM 2006: Int. Symp. on Formal Methods, volume 4085 of LNCS, pages 460–475. Springer, 2006.

[11] National Institutes of Standard Technologies, Planning Report 02-3 The Economic Impacts of Inadequate Infrastructure for Software, 2002

[12] Guide ADR (Analyse de risques) pour ESPN N1, AFCEN, 2018

[13] INCOSE Systems Engineering Handbook: A Guide for System Life Cycle Processes and Activities, 4th Edition, INCOSE, 2015

[14] Chomsky, Noam. "Three models for the description of language". IRE Transactions on Information Theory, 1956