# Vers une traduction de K en Dedukti

Amélie Ledein, Valentin Blot, Catherine Dubois

► To cite this version:

Amélie Ledein, Valentin Blot, Catherine Dubois. Vers une traduction de K en Dedukti. JFLA 2022 - Journées Francophones des Langages Applicatifs (JFLA), Jun 2022, Saint-Médard-d'Excideuil, France. hal-03604962

HAL Id: hal-03604962

https://hal.science/hal-03604962

Submitted on 10 Mar 2022

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
Vers une traduction de K en DEDUKTI

Amélie Ledein¹*, Valentin Blot¹, Catherine Dubois²

¹ Laboratoire Méthodes Formelles, Inria, Université Paris-Saclay

² Samovar, ENSIIE

K est un *framework* sémantique permettant de décrire formellement des sémantiques de langages de programmation. C'est aussi un environnement qui offre différents outils pour aider à la programmation avec les langages spécifiés dans le formalisme. Il est par exemple possible d'exécuter des programmes ou encore de vérifier certaines propriétés sur ceux-ci à l'aide de l'outil KPROVER. K repose sur une logique du 1er ordre munie d'une application entre formules et d'opérateurs de point fixe, d'égalité, de typage ainsi que d'un opérateur similaire à l'opérateur "next" des logiques temporelles. Ce dernier opérateur permet d'encoder la sémantique des programmes par la réécriture.

DEDUKTI est un *framework* logique permettant l'interopérabilité des preuves entre différents outils de preuve formelle. Il possède des plugins d'import et d'export pour des systèmes de preuve aussi divers que COQ, PVS ou encore ISABELLE/HOL. Il repose sur le λΠ-CALCUL MODULO THÉORIE, une extension de la théorie des types par l'ajout de règles de réécriture dans la relation de conversion. La flexibilité de ce *framework* logique permet d'encoder de nombreuses théories comme la logique du 1er ordre ou la théorie des types simples.

Dans cet article, nous présentons KAMELO, un outil de traduction de K vers DEDUKTI. Cet outil a pour objectif, à plus long terme, de permettre la vérification des preuves faites au sein de K, et la réutilisation de sémantiques formelles de langages de programmation ainsi que des propriétés sur leurs programmes au sein de nombreux systèmes de preuve, via DEDUKTI.

# 1 Introduction

Les méthodes formelles ont pour principal objectif l'obtention d'une plus grande confiance dans les programmes informatiques. Mais avant même de pouvoir vérifier un programme, celui-ci doit être écrit dans un langage de programmation dont il est indispensable de connaître précisément la syntaxe et la sémantique, et donc de disposer, dans un premier temps, d'une formalisation de la sémantique du langage de programmation utilisé pour écrire le programme que nous souhaitons vérifier. De nombreux outils permettent d'écrire des sémantiques formelles, comme par exemple CENTAUR [12], ASF+SDF [29], OTT [27], SAIL [7], LEM [23] ou encore K [6]. Dans cet article, nous nous intéressons uniquement à ce dernier, puisque actuellement, il existe un grand nombre de sémantiques de langage de programmation écrites en K, comme celles de JAVA [11], C [20] ou encore JAVASCRIPT [24]. Une fois la sémantique d'un langage spécifiée, K offre la possibilité d'exécuter un programme écrit dans ce langage, mais également la possibilité de vérifier certaines propriétés - exprimées sous la forme de propriétés d'atteignabilité - sur ce programme, à l'aide du prouveur automatique KPROVER [28].

Nous nous intéressons à la traduction de sémantiques écrites en K vers DEDUKTI, un *framework* logique permettant l'interopérabilité des preuves entre différents outils de preuve formelle. Cela permettrait d'exécuter au sein de DEDUKTI un programme écrit avec le langage formalisé, de vérifier les preuves établies par le KPROVER, voire faire cette preuve avec DEDUKTI, si le KPROVER a échoué, et aussi de vérifier formellement des propriétés sur le langage formalisé avec K.

<footnote>*L'auteure est financée par DIGICOSME.</footnote>
Cet article s'intéresse à la traduction d'une sémantique écrite en K vers DEDUKTI, afin de pouvoir exécuter dans DEDUKTI des programmes écrits dans le langage décrit par cette sémantique. K offre de nombreuses facilités pour écrire une sémantique, comme par exemple des attributs pour spécifier une stratégie d'évaluation. La sémantique écrite par l'utilisateur est traduite dans le langage intermédiaire nommé KORE, qui sera notre format d'entrée pour la traduction vers DEDUKTI. Nos contributions, présentées dans cet article résident, tout d'abord, dans l'étude systématique du langage intermédiaire KORE. En effet, aucun article n'a été encore publié sur ce sujet, et très peu de documentation existe à ce jour. Nous avons donc échangé avec l'équipe K pour conforter notre compréhension de KORE. De plus, nous formalisons la transformation effectuée par KAMELO, un outil en cours de développement permettant de traduire une sémantique écrite en K dans DEDUKTI. La correction de la traduction n'est pas démontrée dans cet article. Informellement, notre traduction cherche à assurer que le programme exécuté dans le framework K et le programme exécuté dans DEDUKTI ont le même comportement - par exemple, calculent la même valeur ou donnent le même état final - si le langage décrit est déterministe.

La vérification des objets de preuve générés par le KPROVER, ainsi que l'encodage des fondements théoriques de K dans ceux de DEDUKTI ne sont pas traités dans cet article et feront l'objet de travaux futurs. La traduction présentée ici est néanmoins nécessaire pour exécuter un programme et sera réutilisée pour la vérification des preuves.

Après une brève présentation du $\lambda\Pi$-CALCUL MODULO THÉORIE (Section 2) et de son implémentation DEDUKTI (Section 3), nous présentons la logique sous-jacente de K, la MATCHING LOGIC (Section 4), ainsi que le framework K plus en détails, en formalisant un langage impératif nommé IMP (Section 5). Nous expliquons ensuite comment une sémantique K est traduite dans KORE qui est une théorie de la MATCHING LOGIC (Section 6). Enfin, nous présentons l'outil KAMELO qui effectue la traduction de KORE vers DEDUKTI (Section 7).

Dans la suite, les mots-clefs d'un langage ou ce qui est natif dans un langage seront distingués par de la couleur. Le langage de DEDUKTI se différenciera par une **couleur bleue**, le langage K par une **couleur orange**, le langage de KORE par une **couleur rouge**, et le langage de la MATCHING LOGIC par une **couleur verte**. Celles-ci facilitent la lecture, mais ne sont pas nécessaires à la compréhension.

## 2 Le $\lambda\Pi$-calcul modulo théorie

Le $\lambda\Pi$-CALCUL MODULO THÉORIE, abrégé $\lambda\Pi\equiv_T$ par la suite, est un *framework* logique, c'est-à-dire un *framework* permettant de définir des théories, introduit par Cousineau et Doweck [17]. Celui-ci est une extension du $\lambda\Pi$-calcul, avec une notion primitive de calcul définie à l'aide de règles de réécriture [18]. Actuellement, de nombreuses théories ont pu être encodées dans ce framework comme, par exemple, le Calcul des Constructions [10]. La syntaxe, ainsi que les règles de typage<fnref n="1" /> qui régissent le $\lambda\Pi\equiv_T$ sont disponibles en figure 1, où le jugement de typage $\Gamma \vdash t : A$ signifie que le terme $t$ a le type $A$ sous le contexte $\Gamma$. Le jugement spécifique $\Gamma \vdash A : \mathbf{Type}$ indique que $A$ est un type sous le contexte $\Gamma$. Nous considérons également une signature $\Sigma$, ainsi qu'un ensemble de règles de réécriture $\mathcal{R}$. Dans ce cadre, toute règle de réécriture $l \leftrightarrow r \in \mathcal{R}$ vérifie $Var(r) \subseteq Var(l)$, où $Var(p)$ est l'ensemble des variables de $p$, et l'utilisation d'une telle règle de réécriture nécessite que les instanciations $l\sigma$ et $r\sigma$ de ses membres gauche et droit soient toutes deux bien typées, avec le même type ($\Gamma \vdash l\sigma : A$ et $\Gamma \vdash r\sigma : A$ pour un certain type $A$).

<footnote n="1">1. D'après l'isomorphisme de Curry-Howard, ces règles constituent également un système de preuve.</footnote>
<table><thead><tr><th>Syntaxe</th><th>s</th><th>:=</th><th>Type</th><th>Kind</th><th>sorte</th></tr></thead><tbody><tr><td></td><td>t</td><td>:=</td><td>s</td><td>| c</td><td>| x</td><td>| t</td><td>| t</td><td>| λ(x : t) . t</td><td>| Π(x : t) . t</td><td>terme</td></tr><tr><td></td><td>Γ</td><td>:=</td><td></td><td>∅</td><td>| Γ</td><td>, x</td><td>: t</td><td></td><td></td><td>contexte</td></tr><tr><td></td><td>avec</td><td></td><td>c</td><td>une constante</td><td>appartenant à Σ</td><td></td><td></td><td></td><td></td><td></td></tr><tr><td></td><td></td><td></td><td>x</td><td>une variable</td><td></td><td></td><td></td><td></td><td></td><td></td></tr></tbody></table>

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

où $s \in \{\text{Type} ; \text{Kind}\}$, $B\{x\|a\}$ désigne la substitution de $a$ à $x$ dans $B$ et $\equiv_{\beta R}$ est la fermeture réflexive, transitive, symétrique et contextuelle de $\equiv$, générée par les règles $\equiv_{reduc}$ et $\equiv_{rule}$.

<caption>FIGURE 1 – Syntaxe et typage du $\lambda\Pi\equiv_{\tau}$ avec une signature $\Sigma$ et des règles de réécriture $\mathcal{R}$</caption>

Notons que dans la règle de conversion (conv), la relation d'équivalence dépend non seulement de la $\beta$-réduction mais aussi du système de réécriture $\mathcal{R}$. De plus, afin d'avoir la décidabilité du typage, la condition $A \equiv_{\beta R} B$ dans la règle (conv) doit être décidable, ce qui est assuré lorsque les systèmes de réécriture considérés sont confluents et terminent. Enfin, les contextes peuvent contenir des éléments mal formés et l'ordre des éléments n'a pas d'importance. La bonne formation des éléments du contexte n'est assurée que lors de leur utilisation, dans la règle (var). Cette présentation a été démontrée équivalente aux présentations usuelles dans [19].

## 3 Un framework pour la logique : Dedukti

DEDUKTI [9, 2, 3] est un framework logique basé sur le $\lambda\Pi\equiv_{\tau}$. Ces fondements logiques permettent d'encoder au sein de DEDUKTI des logiques très expressives comme le Calcul des Constructions Inductives, en les définissant comme des théories du $\lambda\Pi\equiv_{\tau}$. Cela permet d'assurer une interopérabilité des preuves entre différents outils formels comme Coq ou PVS (Figure 2).

Dans cette section, nous ne présentons que les fonctionnalités disponibles dans DEDUKTI sur lesquelles nous nous appuyons dans la suite et qui permettront de faciliter, ultérieurement, les traductions vers d'autres formalismes.

<figure><img src="image_3.png" /><figcaption>FIGURE 2 – L'approche de DEDUKTI, ayant une philosophie similaire à celle de K, mais pour les preuves</figcaption></figure>
**Organisation d'un développement en Dedukti.** La notion de module n'existe qu'au niveau d'un fichier. Par conséquent, un fichier peut être vu comme un module, mais il n'est pas possible de déclarer un module à l'intérieur d'un fichier. Cependant, il est possible d'importer un ou plusieurs fichiers dans un même fichier, avec les mots-clef *require* et/ou *open*, voire de le renommer avant de l'utiliser par la suite, avec le mot-clef *as*.

**Typage et symboles dans Dedukti.** La syntaxe du $\lambda\Pi\equiv_T$ est directement accessible dans DEDUKTI : TYPE (Kind n'étant pas accessible à l'utilisateur car inféré par le système), $\lambda$ (absraction), $\Pi$ (produit dépendant), mais aussi $\rightarrow$ qui est utilisé lorsque le produit est non-dépendant. La signature peut être définie à partir de symboles constants (constant), c'est-à-dire qui ne peuvent pas être réduits par une règle de réécriture. Si la déclaration d'un symbole est faite avec le mot-clef *symbol* seul, le symbole est dit défini, sans propriété particulière.

**Règles de réécriture dans Dedukti.** Dans DEDUKTI, une règle de réécriture s'écrit **rule LHS $\leftrightarrow$ RHS** dans laquelle les variables sont notées $\$x$, $\$y$, etc. Il est possible d'y utiliser un joker ($\_$) à gauche lorsqu'une variable n'est pas utilisée dans la partie droite. Pour des raisons d'efficacité, il est possible de déclarer plusieurs règles à la fois à l'aide du mot-clef **with**. Les règles de réécriture autorisent l'ordre supérieur, peuvent être non linéaires et ne s'appliquent pas forcément en tête de terme, mais ne sont pas conditionnelles. Toutes les règles de réécriture définies dans DEDUKTI constituent un unique ensemble : il n'y a pas de notion de priorité entre ces différentes règles, lorsque nous cherchons la prochaine règle qui s'applique.

# 4 La Matching Logic

Le framework $\mathcal{K}$ a d'abord été développé pour faciliter l'écriture de sémantiques, avec l'objectif de ne garder que le meilleur des différents styles de définition sémantique. Ensuite, la recherche de fondements théoriques pour ce framework a donné lieu à différentes logiques qui s'améliorent les unes les autres [26, 28, 16, 15]. Ici, nous nous inspirons de la présentation de la MATCHING LOGIC faite à ISR 2021 [5] et de l'article [14]. Ainsi une définition sémantique en $\mathcal{K}$ peut être considérée comme une théorie de la MATCHING LOGIC. D'autres formalisations de la sémantique de $\mathcal{K}$ ont été proposées dans la littérature. Par exemple, Li et Gunter proposent une formalisation de la sémantique de $\mathcal{K}$ en ISABELLE/HOL [21, 22]. De plus, il existe des travaux sur la définition de la sémantique de $\mathcal{K}$ en $\mathcal{K}$ [1], et plus récemment, la MATCHING LOGIC a été formalisée à l'aide de METAMATH [13].

**Syntaxe.** La MATCHING LOGIC est une logique non typée du 1er ordre qui suit la philosophie « terms as formulae », c'est-à-dire telle qu'il n'y a pas de distinction entre les termes et les formules. En effet, cette logique manipule des patterns. Soit $\Sigma$ un ensemble de symboles constants, nommé également signature. L'ensemble des $\Sigma$-patterns est défini à l'aide de huit constructeurs : les variables d'élément ($x$), les variables d'ensemble ($X$), les symboles ($\sigma$), l'application ($\varphi_1 \ \varphi_2$), les connecteurs propositionnels ($\perp$ et $\rightarrow$), le quantificateur existentiel ($\exists x.\varphi$) et l'opérateur de plus petit point fixe ($\mu X.\varphi$, où il n'y a pas d'occurrences négatives de $X$ dans $\varphi$).

**Notations.** Il est possible d'introduire quelques notations, sans étendre l'expressivité de la logique. Nous avons regroupé différentes notations usuelles à la figure 3, en notant $\varphi[\psi/v]$ la substitution du pattern $\psi$ à $v$, une variable d'élément ou d'ensemble, dans le pattern $\varphi$.

**Sémantique.** Le nom de la logique est étroitement lié à la notion de *pattern-matching*, d'où le vocabulaire et la sémantique associés. Intuitivement, un pattern $\varphi$ est interprété par l'ensemble des éléments qu'il matche. La sémantique associée à chaque constructeur de pattern est donc étroitement liée à des opérations usuelles sur les ensembles. Nous notons $\Sigma$-modèle, un triplet $(M, @_M, \{\sigma_M\}_{\sigma \in \Sigma})$ où $M$ est un ensemble support non vide, $@_M$ est l'interprétation du pattern applicatif, de type $M \times M \rightarrow \mathcal{P}(M)$ et $\sigma_M$ est l'interprétation des symboles telle que
<table><thead><tr><th>Constructeur</th><th>Sémantique</th></tr></thead><tbody><tr><td>x</td><td>|x|<sub>M,ρ</sub> = {ρ(x)}</td></tr><tr><td>X</td><td>|X|<sub>M,ρ</sub> = ρ(X)</td></tr><tr><td>σ</td><td>|σ|<sub>M,ρ</sub> = σ<sub>M</sub></td></tr><tr><td>ϕ<sub>1</sub> ϕ<sub>2</sub></td><td>|ϕ<sub>1</sub> ϕ<sub>2</sub>|<sub>M,ρ</sub> = ⋃<sub>a<sub>1</sub>∈|ϕ<sub>1</sub>|<sub>M,ρ</sub><br>a<sub>2</sub>∈|ϕ<sub>2</sub>|<sub>M,ρ</sub></sub> a<sub>1</sub> @ a<sub>2</sub></td></tr><tr><td>⊥</td><td>|⊥|<sub>M,ρ</sub> = ∅</td></tr><tr><td>→</td><td>|ϕ<sub>1</sub> → ϕ<sub>2</sub>|<sub>M,ρ</sub> = M \ (|ϕ<sub>1</sub>|<sub>M,ρ</sub> \ |ϕ<sub>2</sub>|<sub>M,ρ</sub>)</td></tr><tr><td>∃x.ϕ</td><td>|∃x.ϕ|<sub>M,ρ</sub> = ⋃<sub>a∈M</sub> |ϕ|<sub>M,ρ[a/x]</sub></td></tr><tr><td>μX.ϕ</td><td>|μX.ϕ|<sub>M,ρ</sub> = lfp(A ↦ |ϕ|<sub>M,ρ[a/X]</sub>)</td></tr></tbody></table>

<table><caption>FIGURE 3 – Syntaxe, notation et sémantique de la MATCHING LOGIC</caption><thead><tr><th>Notation</th><th>Définition</th></tr></thead><tbody><tr><td>¬ϕ<sub>1</sub></td><td>ϕ<sub>1</sub> → ⊥</td></tr><tr><td>⊤</td><td>¬⊥</td></tr><tr><td>ϕ<sub>1</sub> ∨ ϕ<sub>2</sub></td><td>¬ϕ<sub>1</sub> → ϕ<sub>2</sub></td></tr><tr><td>ϕ<sub>1</sub> ∧ ϕ<sub>2</sub></td><td>¬(¬ϕ<sub>1</sub> ∨ ¬ϕ<sub>2</sub>)</td></tr><tr><td>ϕ<sub>1</sub> ↔ ϕ<sub>2</sub></td><td>(ϕ<sub>1</sub> → ϕ<sub>2</sub>) ∧ (ϕ<sub>2</sub> → ϕ<sub>1</sub>)</td></tr><tr><td>∀x.ϕ</td><td>¬∃x.¬ϕ</td></tr><tr><td>νX.ϕ</td><td>¬μX.¬ϕ[¬X/X]</td></tr></tbody></table>

∀σ ∈ Σ. σ<sub>M</sub> ⊆ M. Cette définition montre que la MATCHING LOGIC a une interprétation ensembliste, alors que la logique des prédicats a une interprétation fonctionnelle, ce qui en fait un cas particulier, en considérant qu'il y a une bijection entre a et {a}. Les sémantiques, notées |.|<sub>M,ρ</sub>, pour les constructeurs sont données à la figure 3, où ρ une valuation telle que ρ(x) ∈ M pour toute variable d'élément x et ρ(X) ⊆ M pour toute variable d'ensemble X. et lfp est une fonction de plus petit point fixe. Les sémantiques pour les notations peuvent être retrouvées par le calcul.

**Théories.** Tout comme le λΠ≡<sub>τ</sub>, la MATCHING LOGIC est une logique permettant de raisonner modulo une théorie. Il est donc tout à fait possible d'ajouter à la MATCHING LOGIC la théorie de l'égalité à l'aide du symbole [−] (definedness symbol), la théorie des sortes à l'aide du symbole [[−]] (inhabitant symbol) ou encore la théorie de la réécriture à l'aide de la sorte State et du symbole • (one-path next symbol). La sémantique de ce dernier symbole repose sur le fait que les règles de réécriture définissent une relation binaire R entre des états, qui sont de type State, c'est-à-dire qu'elles définissent un système de transition.

Les définitions et sémantiques nécessaires sont présentées en figure 4, où [[s]]<sub>M</sub> est l'ensemble support de s dans M.

<table><thead><tr><th>Théorie</th><th>Symbole</th><th>Sémantique</th><th>Axiome</th></tr></thead><tbody><tr><td>Égalité</td><td>|ϕ|</td><td>|[ϕ]| = M si |ϕ| ≠ ∅, |[ϕ]| = ∅ sinon</td><td>∀x. |x|</td></tr><tr><td>Sortes</td><td>[[s]]</td><td>[[s]] = [[s]]<sub>M</sub></td><td></td></tr><tr><td>Réécriture</td><td>State<br>•ϕ</td><td>State est une sorte donc |[State]| = |[State]|<sub>M</sub><br>|•ϕ| = {s ∈ [[State]] | ∃t ∈ |ϕ| tel que s ↦ t ∈ R}</td><td></td></tr></tbody></table>

$$[\varphi] \equiv \neg[\neg\varphi] \quad \varphi_1 \subseteq \varphi_2 \equiv [\varphi_1 \to \varphi_2] \quad \varphi_1 = \varphi_2 \equiv [\varphi_1 \leftrightarrow \varphi_2] \quad x \in \varphi \equiv [x \wedge \varphi] \quad \neg_s \varphi \equiv (\neg\varphi) \wedge [[s]]$$

$$\forall x : s.\varphi \equiv \forall x.(x \in [[s]]) \to \varphi \quad \varphi_1 \leftrightarrow \varphi_2 \equiv \varphi_1 \to \bullet\varphi_2 \quad \diamond\varphi \equiv \mu X.\varphi \lor \bullet X \quad \varphi_1 \leftrightarrow^* \varphi_2 \equiv \varphi_1 \to \diamond \varphi_2$$

<caption>FIGURE 4 – Extensions de la MATCHING LOGIC</caption>

Ces trois théories constituent la théorie nommée KORE, où State est le type des configurations.

**Système de preuve.** Le système de preuve de la MATCHING LOGIC est présenté en figure 5, où C, C<sub>1</sub>, C<sub>2</sub> sont des contextes applicatifs, respectant la grammaire C ::= □ | C ϕ | ϕ C. A travers l'axiome (Prop 3), nous constatons que la MATCHING LOGIC est une logique classique.
<figure><img src="image_4.png" /><figcaption>FIGURE 5 – Système de preuve de la MATCHING LOGIC</figcaption></figure>

## 5 Un framework pour la sémantique : K

Le framework K [6] permet de définir des sémantiques formelles de langages de programmation et de générer automatiquement des outils pour un langage à partir de sa sémantique formelle (Figure 6). Créé par Grigore Rosu en 2003 à l'Université de Champaign-Urbana (USA - Illinois), K est aujourd'hui maintenu par l'entreprise Runtime Verification. Actuellement, les principaux backends sont le backend LLVM pour l'exécution, et le backend HASKELL pour l'exécution symbolique.

<figure><img src="image_5.png" /><figcaption>FIGURE 6 – L'approche de K</figcaption></figure>

Il est possible de considérer K comme une sur-couche orientée notation au-dessus de la logique de réécriture, spécialisée et optimisée pour écrire les définitions de langages et de modèles de programmation complexes. Pour illustrer les fonctionnalités de K, nous allons montrer comment écrire la sémantique d'un petit langage impératif que nous nommons IMP. Pour une présentation plus complète, le lecteur peut se rapporter à [25].

**Organisation d'un développement en K.** Contrairement à DEDUKTI, la notion de fichier est disjointe de la notion de module puisqu'un fichier peut contenir plusieurs modules (module/endmodule). De plus, il est possible d'importer des fichiers dans un autre fichier (requires), ou encore d'importer un ou plusieurs modules dans un autre module (imports).
Pour finir, la sorte *K* indique qu'un élément de type *K* est calculatoire : tout ce qui est défini dans *K* est de type *K*. Les *K* computations sont un cas particulier de contenu calculatoire, donc de type *K*, particulièrement utiles pour définir des stratégies d'évaluation. Formellement, une *K* computation est une liste, potentiellement imbriquée et ayant pour constructeurs `∩` et `∠`, de calculs à réaliser de manière séquentielle. Par exemple, la *K* computation $x = 10$; `∩` y = 42; modélise le fait que nous affectons d'abord une valeur à la variable *x* avant de modifier *y*.

**Configurations.** Formellement, une configuration est un multi-ensemble de cellules étiquetées, potentiellement imbriquées. Plus concrètement, une configuration contient toutes les informations sémantiques nécessaires pour exécuter un programme : nous pouvons voir une configuration comme un état du programme, qui stocke par exemple le programme à exécuter, les valeurs courantes des variables ou encore la pile. Pour le langage IMP, nous nous contentons d'une configuration à deux cellules, l'une étiquetée par *k* contenant le programme à exécuter, l'autre étiquetée par env contenant les valeurs courantes des variables. Pour définir une telle configuration en *K*, il suffit de spécifier la configuration initiale souhaitée, comme par exemple configuration <k>$PGM$ : Pgm</k> <env> . Map</env> qui indique que le programme à exécuter ($PGM$) doit être mis dans la cellule *k* et que l'environnement est initialement vide. Dans la suite de cet article, et en accord avec les notations usuelles utilisées dans les articles sur *K*, nous allégeons la notation pour décrire une configuration, comme ⟨⟨ $x$ = 10; $⟩_k$ $⟨$ $x$ $\mapsto$ 0 $⟩_{env}$⟩.

**Règles de réécriture.** Dans $\mathcal{K}$, une règle de réécriture, notée **rule LHS** => **RHS**, est du 1er ordre et s'applique sur des configurations. Par exemple, la règle suivante signifie que la variable $x$ est évaluée à $i$ puisque la valeur associée à $x$ dans l'environnement, ici la cellule **env**, est $i$: **rule ⟨⟨ x ∩ s $⟩_k$ ⟨m $x$ $\mapsto$ i $⟩_{env}$⟩ => ⟨⟨ i ∩ s $⟩_k$ ⟨m $x$ $\mapsto$ i $⟩_{env}$⟩** (règle n°1 - Figure 7).

Comme dans DEDUKTI, les règles de réécriture de $\mathcal{K}$ peuvent être non-linéaires, et ne s'appliquent pas forcément en tête de terme, c'est-à-dire sur une configuration entière. C'est le cas de la règle n°3 (Figure 7) qui donne la sémantique de l'opérateur "+". Dans ce cas de figure, le reste de la configuration est inféré par $\mathcal{K}$ lors de la compilation en KORE. Cette écriture permet de faire des raisonnements locaux, mais permet surtout d'être plus modulaire. Si l'utilisateur souhaite qu'une règle de réécriture puisse être appliquée n'importe où comme dans DEDUKTI, il lui suffit d'ajouter l'attribut **anywhere** à cette règle. De plus, ce qui n'est pas utilisé dans le membre droit peut être omis à l'aide d'un joker, comme aux règles n°7, 10 et 12 (Figure 7).

Contrairement à DEDUKTI, une règle de réécriture peut être conditionnelle dans $\mathcal{K}$, comme le montre la règle n°2 (Figure 7) qui définit la sémantique de la division.

**Définir une stratégie d'évaluation.** Il existe deux attributs pour définir une stratégie d'évaluation, c'est-à-dire préciser l'ordre dans lequel les sous-expressions sont évaluées : **strict**, si elle s'effectue de manière non déterministe, et **seqstrict** si elle s'effectue de manière déterministe, de gauche à droite par défaut. Il est également possible de restreindre la liste des arguments qui doivent être évalués avant l'évaluation de l'instruction globale en donnant une liste de nombres, chacun indiquant la position d'un symbole non terminal. Par exemple, pour définir un « et paresseux », nous pouvons utiliser l'attribut **strict(1)**, ainsi que les deux règles suivantes : **rule true** and **b** => **b** et **rule false** and _ => **false**** (règles n°11 et n°12 - Figure 7).

Enfin, pour spécifier des stratégies d'évaluation plus complexes, il est également possible d'utiliser des contextes (**context**), comme cela se fait classiquement, mais également des squelettes de contextes (**context alias**), permettant de générer automatiquement des contextes, plutôt que d'écrire systématiquement toujours les mêmes contextes. Nous verrons à la section 6.2 une dernière méthode pour définir une stratégie d'évaluation, à l'aide des K computations.
**D'autres attributs.** Il existe de très nombreux attributs 3, mais à notre connaissance, il n'existe pas de liste d'attributs exhaustive totalement documentée. Nous présentons, ci-dessous, les derniers attributs qui nous intéressent dans le cadre de ce travail.

Tout symbole est soit un symbole de constructeur (**constructor**), soit un symbole de fonction (**function**), mais pas les deux. Par défaut, un symbole est un symbole de constructeur. Nous verrons que la différence entre ces deux attributs influence la traduction de K vers KORE, comme le fait que le reste de la configuration est inféré uniquement si le symbole de tête a l'attribut **constructor**. De plus, il est possible de préciser qu'un symbole est injectif (**injective**) ou encore total (**functional**). Enfin, un symbole peut être manipulé modulo associativité (**assoc**), commutativité (**comm**), unité 4 (**unit**), idempotence (**idem**). Ces quatre derniers attributs permettent de faire de la réécriture modulo ACUI.

Les règles de réécriture, par défaut, ne s'appliquent pas dans un ordre particulier. Cependant, l'attribut *owise* indique qu'une règle ne s'applique que lorsque aucune autre ne s'applique, et l'attribut *priority(*nb*)* permet de préciser l'ordre d'application des règles.

# 6 De K à la Matching Logic : Kore

Le langage KORE est un langage intermédiaire entre le langage de K et le langage de la MATCHING LOGIC, permettant ainsi de minimiser l'écart entre le langage qui décrit la sémantique, celui de K, et le langage qui constitue les fondements logiques de K, la MATCHING LOGIC. La compilation d'une définition sémantique en K génère un fichier au format KORE. Notre traduction de K en DEDUKTI, présentée à la section 7, utilise ce format KORE intermédiaire, et non le fichier source écrit en K. Nous supposons donc correcte la traduction de K vers KORE. Cette section explique comment s'effectue cette traduction entre K et la MATCHING LOGIC, explications qui résultent d'une étude des fichiers KORE générés et de discussions avec des membres de l'équipe de développement, puisque aucun document formalisant cette étape n'a été publié. La formalisation partielle de cette traduction est disponible à la figure 8.

**Organisation d'un développement en Kore.** Un fichier KORE est composé d'une succession de modules (**module/endmodule**), commençant éventuellement par des déclarations d'importation (**import**), elles-mêmes suivies de déclarations commençant par l'un des mot-clefs suivants : **sort**, **hooked-sort**, **symbol**, **hooked-symbol**, **alias**/**where**, **axiom**. Quelle que soit la hiérarchie des fichiers qui constitue la sémantique d'un langage, le processus de compilation vers KORE va tout fusionner dans un unique module. Quatre modules 5 sont également importés par défaut lors de la traduction de K vers KORE : **BASIC-K** qui contient les sortes **SortK** et **SortKItem**, correspondant aux sortes **K** et **KItem** dans K; **KSEQ** qui contient les constructeurs des K computations **kseq** et **dotk**, notés ∩ et . dans K; **INJ** qui introduit le symbole **inj** pour modéliser des injections et enfin, K qui contient principalement les modules précédents. Le module K est importé dans le module qui contient la sémantique.

**Notion de typage.** Lors de la traduction de K à KORE, tous les types sont précisés à l'aide d'injections (**inj**), informations de typage que nous utilisons parfois, comme à la section 7.3.

## 6.1 Traduction de la syntaxe dans Kore

La traduction de K vers KORE procède de deux manières différentes selon la forme de B dans une déclaration **syntax A** **::=** B, comme le montre la figure 8 6. Si B n'a pas de symbole

<footnote n="3">3. Une liste non exhaustive est présente à la fin de cette page https://kframework.org/USER_MANUAL/.</footnote>

<footnote n="4">4. On parle aussi d'identité, c'est-à-dire modulo les éléments neutres.</footnote>

<footnote n="5">5. Les modules **BASIC-K**, **KSEQ**, **INJ** et **K** sont disponibles ici : https://github.com/kframework/kore/blob/master/src/main/kore/prelude.kore, ou au chemin "/usr/include/kframework/builtin/prelude.md".</footnote>

<footnote n="6">6. Dans cette figure, de nombreuses déclarations introduisent des accolades laissées vides. En effet, de très rares cas nécessitent de traduire les paramètres de type mis entre accolades.</footnote>
**Module et importation** ($I_j^h$ est de la forme **imports** $I_j^h$ [ ]), $k \ge 1$ et $\forall j. n_j \ge 0$

|| module $I_1^1$ ... $I_{n_1}^1$ $M_1$ **endmodule** ... module $I_1^k$ ... $I_{n_k}^k$ $M_k$ **endmodule** ||**kore** =

|| Prelude ||**aux** module **import K** [ ] || $M_1$ ||**kore** ... || $M_k$ ||**kore** **endmodule** [ ]

|| Prelude ||**aux** = Modules BASIC-K, KSEQ, INJ et K

**Syntaxe** (A est un symbole non terminal)

|| **syntax** A : := B [Attr] ||**kore** =
|| **sort** A{} [ ] ||**aux**
|| **sort** B{} [ ] ||**aux**
**axiom** $\varphi_{B \subseteq A}$ [**subsort**]

|| **syntax** A : := B [Attr] ||**kore** =
|| **sort** A{} [ ] ||**aux**
|| **symbol** B{}($T_1$, ..., $T_m$) : A [Attr] ||**aux**

Si B est de la forme $X_1 X_2 \dots X_n$
avec $n \ge 1$ et $X_i$ un symbole,
et $\forall i \in [1..m] \exists j. X_j = T_i$
avec $T_i$ un symbole non terminal.

|| **sort** A{} [ ] ||**aux** =
|| **sort** A{} [ ]
|| **Proj_A** et **Pred_A** ||**aux**

Si A n'est pas dans
la bibliothèque de K.

|| **sort** A{} [ ] ||**aux** =
|| **hooked-sort** A{} [ ]
|| **Proj_A** et **Pred_A** ||**aux**

Si A est dans
la bibliothèque de K.

|| **Proj_A** et **Pred_A** ||**aux** =
|| **symbol** projectA{}(...) : A [**projection**] ||**aux**
|| **symbol** isA{}(...) : **SortBool** [**predicate**] ||**aux**

Si A $\ne$ **SortKConfigVar**.

|| **symbol** B{}($T_1$, ..., $T_m$) : A [x, ...] ||**aux** =
|| **symbol** B{}($T_1$, ..., $T_m$) : A [x, ...]
**axiom** $\varphi_x$ [x, ...]

Si $x \in \{\text{assoc, comm, unit, idem}$
functional, constructor, injective,
projection, predicate, initializer $\}$.

**Configuration**

|| **configuration** C ||**kore** =
|| **sort** Sortcell{} [ ] ||**aux**
Où cell $\in C$.

|| **symbol** Initcell{} [**initializer**] ||**aux**
|| **sort** SortKConfigVar {} [ ] ||**aux**

Si $\$PGM$ est une valeur d'initialisation.

**Règle de réécriture**

|| **rule** LHS $\Rightarrow$ RHS **requires** Cond [Attr] ||**kore** =
**alias** A{}($T_1$, ..., $T_n$) : $T_e$ **where** A{}($N_1$ : $T_1$, ..., $N_n$ : $T_n$)
$:= \overline{\text{Cond}^\varphi} \wedge \text{mgCONF}(\overline{\text{LHS}^\varphi})$ [ ]
**axiom** A{}($N_1$ : $T_1$, ..., $N_n$ : $T_n$) $\leftrightarrow$
$\top \wedge \text{mgCONF}(\overline{\text{RHS}^\varphi})$) [Attr]

Si le symbole de tête a l'attribut **constructor**.
Où A est un alias pour LHS,
$T_1, \dots, T_n$ correspondent aux
types des variables de LHS,
et $T_e$ est le type de LHS.

|| **rule** LHS $\Rightarrow$ RHS **requires** Cond [Attr] ||**kore** =
**axiom** $\overline{\text{Cond}^\varphi} \wedge \text{Data} \rightarrow$
($\overline{\text{LHS}^\varphi} = (\overline{\text{RHS}^\varphi} \wedge \top)$) [Attr]

Si le symbole de tête a l'attribut **function**.
Où Data décrit des associations
entre des variables et des patterns.

**Stratégie d'évaluation**

|| **syntax** A : := B [**strict**, Attr] ||**kore**
Voir section 6.2 pour

|| **syntax** A : := B [**seqstrict**, Attr] ||**kore**
des exemples de transformation

|| **context** Co ||**kore**
en K computations.

|| **context** alias CA ||**kore**

<caption>FIGURE 8 – Règles de traduction de K vers KORE</caption>
terminal, comme dans `syntax AExp ::= Int`, alors il est généré une sorte `B` ainsi qu’un *axiome de sous-typage* ayant l’attribut `subsort`, précisant que `B` est une sous-sorte de `A`, noté $\varphi_{B \subseteq A}$.
Mais si `B` a au moins un symbole terminal, comme dans `syntax AExp ::= AExp "-" AExp`, alors est introduit un symbole `B` qui conserve les attributs précisés par l’utilisateur. De plus, pour chaque sorte générée, sont ajoutés un symbole de projection <fnref n="7" />, ayant l’attribut `projection`, permettant de projeter une entité de type `SortK` vers un autre sous-type, ainsi qu’un symbole de prédicat, comme `isBool`, ayant l’attribut `predicate`, indiquant qu’une entité est du type associé au symbole de prédicat.

## 6.2 Traduction de la sémantique dans Kore

**Configurations.** La configuration initialement déclarée dans $K$ est découpée en plusieurs morceaux, un morceau par cellule. Chaque cellule <fnref n="8" /> génère une sorte pour typer la cellule, ainsi qu’un symbole avec au moins l’attribut `cell` pour la représenter. De plus, la configuration initiale précise la valeur d’initialisation de chaque cellule, ce qui génère un symbole avec l’attribut ` initializer`, correspondant à cette valeur d’initialisation.

**Règles de réécriture.** La traduction vers KORE d’une règle de réécriture de la forme `rule LHS => RHS requires C_{pre} [Attr] génère un alias (alias/where) du LHS utilisé dans un axiome commençant par $\leftrightarrow$`, si le symbole de tête possède l’attribut `constructor`. Cet axiome encode la règle de réécriture de la manière suivante : $C_{pre} \wedge LHS \leftrightarrow RHS$ <fnref n="9" />. Si la clause `requires C_{pre}` est omise, alors $\overline{C_{pre}}^\varphi$ devient $\top$ lors de la traduction. Si le symbole de tête possède l’attribut `function`, l’encodage est similaire mais l’axiome commence par $\rightarrow$. La formalisation de ces traductions sont disponibles à la figure 8, où la fonction $\overline{f}^\varphi$ transforme $f$ en un pattern de la MATCHING LOGIC, et la fonction `mgCONF` calcule le reste de la configuration. Si la règle possède l’attribut `anywhere`, la fonction `mgCONF` est l’identité.

**Stratégies d’évaluation.** Nous avons vu en section 5.2 trois manières différentes de définir des stratégies d’évaluation dans $K$: les attributs `strict` et `seqstrict`, les contextes et les contextes alias. Lors de la traduction vers KORE, les attributs `strict` et `seqstrict`, mais aussi les contextes et les contextes alias sont traduits en utilisant les K computations et des *freezers*. Intuitivement, un freezer permet de « geler » le reste de la K computation, qui devient non-modifiable, en attendant que la tête de la K computation soit évaluée. Par la suite, nous notons (`*nb sym` arg) un freezer où `sym` est un symbole, `nb` le numéro de l’argument dont nous attendons la valeur, et `arg` la liste des autres arguments. Par exemple, pour calculer `(4 + 8) - 10`, nous construisons la liste `4 + 8 \frown (*1_\_ 10)` puisque nous souhaitons d’abord évaluer ce qui se trouve entre parenthèses. Nous obtenons ensuite `12 \frown (*1_\_ 10)` car nous commençons d’abord par calculer le premier élément de la liste, puis nous « dégelons » le calcul pour obtenir `12 - 10`, et enfin 2. Cette notion est inspirée des contextes d’évaluation $C[v]$, et des continuations $v \frown C$ (passer $v$ à la continuation $C$).

Dans le cas du « et paresseux » du langage IMP, l’attribut `strict(1)` génère la règle de réécriture `rule E₁ and E₂ => E₁ \frown (*1_{and} E₂) requires E₁ \notin KResult`, mais aussi la règle symétrique `rule E₁ \frown (*1_{and} E₂) => E₁ and E₂ requires E₁ \in KResult`. La sorte `KResult` est une sous-sorte de K qui permet de distinguer les valeurs (finales) des expressions. Pour IMP, nous

<footnote n="7">7. Sauf pour `SortKConfigVar`, la sorte des variables de configuration de $K$, comme la variable `$PGM`.</footnote>

<footnote n="8">8. Certaines cellules sont ajoutées par rapport à celles précisées par l’utilisateur, comme la cellule `<generatedTop>` qui encapsule toutes les autres cellules. Le processus décrit est le même, outre que l’attribut `cell` devient `cellFragment`, et l’attribut `initializer` devient `cellOptAbsent`, puisque cette cellule n’a pas de valeur initiale.</footnote>

<footnote n="9">9. Les propriétés autorisées par le KPROVER sont de la forme `rule LHS => RHS requires C_{pre} ensures C_{post}` et sont encodées ainsi : $C_{pre} \wedge LHS \leftrightarrow C_{post} \wedge RHS$. Dans le cadre de cet article, $C_{post}$ vaut donc $\top$, comme le montre la figure 8.</footnote>
définissons cette sorte ainsi `syntax KResult ::= Int | Bool`, c'est-à-dire qu'une valeur finale est soit un entier, soit un booléen. Ainsi, la première règle force l'évaluation de $E_1$ si $E_1$ n'est pas une valeur, tandis que la deuxième règle simplifie la K computation puisque son élément de tête est une valeur. La condition $E_1 \in KResult$ devient `isKResult E_1` dans le format KORE. D'autres exemples de traduction des attributs définissant une stratégie d'évaluation utilisés à la figure 7 sont disponibles à la figure 9.

<table><caption>FIGURE 9 – Traduction des attributs `strict` et `seqstrict` dans KORE</caption><thead><tr><th>Règles générées par l'attribut strict</th><th>Règles générées par l'attribut seqstrict</th></tr></thead><tbody><tr><td>rule E<sub>1</sub> + E<sub>2</sub> => E<sub>1</sub> ∩ (*<sub>+</sub><sup>1</sup> E<sub>2</sub>) requires E<sub>1</sub> &notin; KResult</td><td>rule E<sub>1</sub> &lt; E<sub>2</sub> => E<sub>1</sub> ∩ (*<sub>&lt;</sub><sup>1</sup> E<sub>2</sub>) requires E<sub>1</sub> &notin; KResult</td></tr><tr><td>rule E<sub>1</sub> ∩ (*<sub>+</sub><sup>1</sup> E<sub>2</sub>) => E<sub>1</sub> + E<sub>2</sub> requires E<sub>1</sub> &in; KResult</td><td>rule E<sub>1</sub> ∩ (*<sub>&lt;</sub><sup>1</sup> E<sub>2</sub>) => E<sub>1</sub> &lt; E<sub>2</sub> requires E<sub>1</sub> &in; KResult</td></tr><tr><td>rule E<sub>1</sub> + E<sub>2</sub> => E<sub>2</sub> ∩ (*<sub>+</sub><sup>2</sup> E<sub>1</sub>) requires E<sub>2</sub> &notin; KResult</td><td>rule E<sub>1</sub> &lt; E<sub>2</sub> => E<sub>2</sub> ∩ (*<sub>&lt;</sub><sup>2</sup> E<sub>1</sub>)<br>requires E<sub>2</sub> &notin; KResult &and; E<sub>1</sub> &in; KResult</td></tr><tr><td>rule E<sub>2</sub> ∩ (*<sub>+</sub><sup>2</sup> E<sub>1</sub>) => E<sub>1</sub> + E<sub>2</sub> requires E<sub>2</sub> &in; KResult</td><td>rule E<sub>2</sub> ∩ (*<sub>&lt;</sub><sup>2</sup> E<sub>1</sub>) => E<sub>1</sub> &lt; E<sub>2</sub> requires E<sub>2</sub> &in; KResult</td></tr></tbody></table>

**Attributs.** Les attributs initialement présents dans le fichier K sont a priori recopiés dans le fichier KORE. Certains attributs pouvant être associés à un symbole génèrent également un axiome, comme le montre la figure 8. Deux cas particuliers existent. Pour l'attribut `predicate`, deux axiomes sont générés au lieu d'un seul, l'un précisant la sémantique quand le prédicat se réduit à faux, l'autre dans le cas vrai. Pour l'attribut `constructor`, un axiome d'injectivité est généré pour chaque symbole ayant cet attribut, ainsi que deux axiomes pour chaque ensemble de constructeurs construisant une valeur d'un même type : un axiome de non-recouvrement, précisant que deux valeurs d'un certain type commençant par des constructeurs différents sont différentes; et un axiome d'exhaustivité, précisant que nous ne pouvons construire des valeurs d'un certain type qu'avec les constructeurs associés à ce type.

Tout axiome généré est la formalisation de la sémantique que nous avons décrite précédemment de manière informelle pour chaque attribut associé à un symbole. Nous verrons dans la partie suivante, comment tous ces axiomes sont traduits dans DEDUKTI.

Enfin, de très nombreux symboles rattachés à la bibliothèque standard de K (`hooked-symbol`) sont également ajoutés dans le fichier KORE. Leur règle de traduction est similaire au cas `symbol`: en fonction des attributs qu'ils possèdent, certains axiomes seront générés. Cependant, certains de ces symboles semblent uniquement utiles à des backends particuliers de K.

# 7 Traduire Kore dans Dedukti

Cette section s'intéresse à l'outil KAMELO [4] en cours de développement. Nous présentons une formalisation de la traduction effectuée par cet outil, c'est-à-dire les encodages superficiels réalisés, et formalisés à la figure 10. Une version en K, en KORE et en DEDUKTI de IMP, est également disponible avec le code source de KAMELO.

## 7.1 Traduction élémentaire

Une très grande majorité des encodages sont assez directs, notamment car K et DEDUKTI partagent un très grand nombre de fonctionnalités, comme les règles de réécriture.

**Module et import.** Tous les modules sont fusionnés dans un unique fichier, en ajoutant le prélude de DEDUKTI après la traduction du module BASIC-K, puisque les déclarations disponibles dans notre prélude dépendent de la sorte `SortK`.

**Sortes et symboles.** La très grande majorité des sortes et des symboles traduits dans le fichier KORE découlent des déclarations `syntax` et `configuration` présentes dans K. Nous constatons que la traduction est très simple : toutes les sortes deviennent des symboles de type `SortK`, sauf la sorte `SortK` elle-même, qui a le type `TYPE`. Pour les symboles, la seule différence est que la signature est currifiée. Les sortes et symboles rattachés à la bibliothèque standard de K doivent également être définis dans le prélude de DEDUKTI : les traductions sont similaires à celles présentées à la figure 10.
**Traduire les axiomes.** Nous notons $X$-axiome, un axiome de la MATCHING LOGIC com-
mençant par l'opérateur $X$. Un $\exists$-axiome possède soit l'attribut **subsort** (*axiome de sous-
typage*), soit l'attribut **functional** (*axiome de fonctionnalité*). Un **=-axiome** est un axiome
équationnel ayant l'attribut **assoc**, **comm**, **unit** ou **idem**. Les $\forall$-axiome et $\perp$-axiome possèdent
l'attribut **constructor** et sont des axiomes d'exhaustivité des constructeurs. Un **$\neg$-axiome
possède** l'attribut **constructor** et est un axiome de non-recouvrement des constructeurs, tan-
dis qu'un **$\rightarrow$-axiome possédant** l'attribut **constructor** est un axiome d'injectivité des construc-
teurs. Les autres **$\rightarrow$-axiomes peuvent** avoir l'attribut **initializer**, **projection**, **predicate
ou aucun attribut**. Un **$\leftarrow$-axiome correspond à une règle de réécriture**.

Seuls les $\leftarrow$-axiome et $\rightarrow$-axiome, n'ayant pas l'attribut constructor, sont traduits. Ils ont été
générés par une règle de réécriture écrite dans $\mathbb{K}$, et seront donc traduits par une ou des règles
de réécriture en DEDUKTI. La traduction $\parallel . \parallel_{CTRS}$ est expliquée aux sections 7.2 et 7.3.

Importation

|| **import** *I* [ ] ||<sub>dk</sub> = nothing

Sorte

|| sort SortK{} [ ] ||<sub>dk</sub> = constant symbol ̂SortK : TYPE

|| sort S{} [ ] ||<sub>dk</sub> = constant symbol ̂S : SortK

|| hooked-sort S{} [ ] ||<sub>dk</sub> = nothing

Si $S \neq \mathbf{SortK}$.

Si $S$ est définie dans le prélude de DEDUKTI.

Symbole

|| **symbol** C{}(*T*₁, ..., *T*ₙ) : *T*ₑ [ **Attr** ] ||<sub>dk</sub> =
**symbol** ̂C : ̂T₁ → ... → ̂Tₙ → ̂Tₑ

|| hooked-symbol C{} [ ] ||<sub>dk</sub> = nothing

Si *C* est définie dans le prélude de DEDUKTI.

Axiome

|| alias A{}(*T*₁, ..., *T*ₙ) : *T*ₑ where A{}(*N*₁ : *T*₁, ..., *N*ₙ : *T*ₙ) := Cond ∧ LHS [ ]
axiom A{}(*N*₁ : *T*₁, ..., *N*ₙ : *T*ₙ) ↪→ ⊤ ∧ RHS [Attr] ||<sub>dk</sub> =

$$
\left\{
\begin{array}{l@{\quad}l@{\quad}l}
\text{rule } \widehat{LHS}^r & \leftarrow \widehat{RHS}^r & \text{si } Cond = \top. \\
\text{|| } (\widehat{LHS}^r, \widehat{RHS}^r, \widehat{Cond}^r) & \parallel_{CTRS} & \text{sinon.}
\end{array}
\right.
$$

|| axiom Ax [ x ] ||<sub>dk</sub> = nothing

Si $x \in \{\text{subsort, functional, constructor, assoc, comm, unit, idem}\}$.

|| axiom Cond ∧ Data →

$$
\begin{array}{l}
(LHS = (RHS \wedge \top)) [Attr] ||_{dk} = \\
\quad \left\{
  \begin{array}{@{}l@{\quad}l@{\quad}l}
    \text{rule } \widehat{LHS}^{Data} \leftarrow \widehat{RHS}^{Data} & \text{si } Cond = \top. & \\
    \text{|| } (\widehat{LHS}^{Data}, \widehat{RHS}^{Data}, \widehat{Cond}^{r}) ||_{CTRS} & \text{sinon.} &
  \end{array}
\right.
\end{array}
$$

Où *Attr* peut être vide ou contenir les attributs
**projection**, **predicate** ou **initializer**.

où $\hat{S}$ transforme l'identificateur $S$ de KORE, en un identificateur de DEDUKTI.

$\hat{S}^r$ transforme le pattern $S$ en un terme de DEDUKTI.

$\hat{S}^{Data}$ transforme le pattern $S$ en un terme de DEDUKTI, en utilisant les associations entre variables et patterns décrites par *Data*.

<caption>FIGURE 10 – Traduction de KORE vers DEDUKTI via KAMELO</caption>

7.2 Traduction des règles de réécriture conditionnelles

Dans cette section, nous nous intéressons à la traduction des règles de réécriture condi-
tionnelles. Comme DEDUKTI ne propose pas la possibilité de définir des règles de réécriture
conditionnelles, il est nécessaire de trouver un encodage d'un système de réécriture condition-
nelle (*CTRS*) vers un système de réécriture non conditionnelle (*TRS*).
### 7.2.1 Encodage sur un exemple

Considérons le système suivant :

(1) rule max X Y => Y requires X <Int Y

(2) rule max X Y => X requires X >=Int Y.

L'encodage permet d'obtenir le système de réécriture suivant dans DEDUKTI :

(0) rule max $x$ $y \leftrightarrow bmax $x$ $y \leftrightarrow b

(1') rule bmax $x$ $y \leftrightarrow $c \leftrightarrow bmax $x$ $y ($$x$$ < $$y$$) $c$

(1'') rule bmax $x$ $y$ true $c$ \leftrightarrow $y

(2') rule bmax $x$ $y$ $c$ \leftrightarrow bmax $x$ $y$ $c$ ($$x$$ \geq $$y$$)

(2'') rule bmax $x$ $y$ $c$ true \leftrightarrow $x.

Avec le système obtenu, $max$ 5 3 se calcule ainsi : $max$ 5 3 $\leftrightarrow_0$ $bmax$ 5 3 $\leftrightarrow b \leftrightarrow_1$ $bmax$ 5 3 (5 < 3) $\leftrightarrow$* $bmax$ 5 3 false $\leftrightarrow_2$ $bmax$ 5 3 false (5 $\ge$ 3) $\leftrightarrow$* $bmax$ 5 3 false true $\leftrightarrow_2$ 5.

L'idée générale de l'encodage, proposé dans cette section et initialement proposée par Viry [30], est d'ajouter, pour un symbole défini avec des règles conditionnelles, autant d'arguments qu'il y a de conditions. La règle (0) réécrit un terme dont le symbole de tête est $max$, par un terme utilisant la version étendue correspondante d'arité 4, $bmax$, où tous les arguments booléens valent $b$, indiquant que les arguments booléens n'ont pas encore été initialisés par une condition. Les règles (1') et (2') initialisent les conditions à calculer, tandis que les règles (1'') et (2'') réduisent la taille du terme puisque une des conditions a été évaluée à true.

Contrairement à Viry, nous choisissons d'étendre la signature, comme ici avec le symbole $bmax$, plutôt que de remplacer chaque symbole de la signature par un symbole équivalent mais avec une arité plus grande, permettant de transporter les calculs des conditions. En effet, cela complique le code et oblige à traduire, après coup, les formes normales obtenues.

De plus, cet encodage a l'avantage de ne pas fixer l'ordre d'évaluation des conditions, mais augmente le temps de calcul, cela en doublant le nombre initial de règles.

Enfin, pour générer les règles précédentes, il faut connaître toutes les conditions qui peuvent s'appliquer, pour un symbole de tête donné. Cependant, de nombreuses règles de réécriture écrites dans $K$, c'est-à-dire celles ayant un symbole de constructeur comme symbole de tête et n'ayant pas l'attribut anywhere, nécessitent d'inférer la configuration. Cela implique que si nous considérons la définition usuelle d'un symbole de tête, ces règles de réécriture auraient le même symbole de tête. Dans le cadre de cet article, nous considérons donc que le symbole de tête d'une règle de réécriture correspond au symbole de tête de la partie du terme gauche de la règle se trouvant dans la cellule $<k>$, sans considérer les symboles dotk, kseq et inj. Si la règle a un symbole de fonction comme symbole de tête ou possède l'attribut anywhere, le symbole de tête correspond au symbole de tête au sens usuel.

Nous notons $head_{<k>}$ la fonction qui renvoie le symbole de tête de la cellule $<k>$, pour une règle donnée, sans considérer les symboles dotk, kseq et inj. Nous notons également $C_σ$, l'ensemble des règles qui partagent le même symbole de tête $σ$, soit $C_σ = \{ l \stackrel{c}{\mapsto} r \mid head_{<k>} (l \stackrel{c}{\mapsto} r) = \sigma \}$.

### 7.2.2 Formalisation de l'encodage

Soit $\mathfrak{R}$ un système de réécriture conditionnelle écrit dans $K$. Pour éviter des conflits de nommage, nous supposons également que $b$ est un nom de symbole non utilisé, et qu'il n'apparaît en tête d'aucun nom de symbole. Nous présentons la traduction notée $||.||_{CTRS}$ précédemment. Celle-ci prend en argument un ensemble $\mathcal{E}_{DK}$ de triplets de termes DEDUKTI de la forme $(LHS, RHS, c)$, noté ici $LHS \stackrel{c}{\mapsto} RHS$, obtenu une fois les traductions $||.||_{KORE}$ et $||.||_{DK}$ appliquées sur $\mathfrak{R}$. Après avoir construit les $C_σ$ à partir de $\mathcal{E}_{DK}$, nous déroulons l'algorithmme présenté à la figure 11, pour chaque $C_σ$, où $X$ est le nombre de règles conditionnelles dans $C_σ$.
1. Si $X = 0$, $C_{\sigma}$ est inchangé et l'algorithme s'arrête. Sinon, initialiser $i$ à 0 et aller en 2.

2. Générer le LHS le plus général pour un symbole $\sigma$ donné, noté $mglhs_{\sigma}$.

3. Générer le symbole étendu $b\sigma$ de type $T_1 \rightarrow \dots \rightarrow T_{n-1} \rightarrow b\text{Bool} \rightarrow \dots \rightarrow b\text{Bool} \rightarrow T_n$, avec $X$ argument(s) de type $b\text{Bool}$, où $b\text{Bool} = \text{Bool} \cup \{b\}$, et $\sigma$ de type $T_1 \rightarrow \dots \rightarrow T_n$.

4. Générer la règle de substitution : $mglhs_{\sigma} \leftrightarrow mglhs_{\sigma}[\text{update}_{same}(\sigma, b\sigma, b)]_{\sigma}$

5. Pour chaque règle appartenant à $C_{\sigma}$ :

(a) Si la règle est de la forme $l \stackrel{c}{\leftrightarrow} r \in C_{\sigma}$ et n'a pas l'attribut *owise* (avec $c \neq \top$) :

— Incrémenter $i$ de 1

— Générer une règle d'initialisation :

$l[\text{update}_{diff}(\sigma, b\sigma, b, i, -)]_{\sigma} \leftrightarrow l[\text{update}_{diff}(\sigma, b\sigma, c, i, -)]_{\sigma}$

— Générer une règle de réduction : $l[\text{update}_{diff}(\sigma, b\sigma, \text{true}, i, -)]_{\sigma} \leftrightarrow r$

(b) Si la règle est de la forme $l \stackrel{\top}{\leftrightarrow} r \in C_{\sigma}$ et n'a pas l'attribut *owise*, générer la règle de réduction : $l[\text{update}_{same}(\sigma, b\sigma, -)]_{\sigma} \leftrightarrow r$.

(c) Si la règle $l \stackrel{\top}{\leftrightarrow} r \in C_{\sigma}$ à l'attribut *owise*, générer la règle de réduction :

$l[\text{update}_{same}(\sigma, b\sigma, \text{false})]_{\sigma} \leftrightarrow r$.

Où :

* $t_1[t_2]_{\sigma}$ signifie que nous substituons $t_2$ au sous-terme ayant pour symbole de tête $\sigma$ dans $t_1$,

* $arg_i(t)$ correspond au $i$-ème argument de $t$ et $arity(t)$ au nombre d'arguments de $t$,

* $mglhs_{\sigma}$ désigne la configuration initiale où les cellules les plus profondes deviennent, $<c> y_i$ si $<c> \neq <k>$, $<k>$ (kseq (inj $\sigma$ $z_1$ ... $z_{arity(\sigma)}$) $L$) sinon, avec $y_i$ et $z_i$ des variables fraîches et, $L$ une K computation.

$$ * update_{diff}(\sigma, b\sigma, s_1, i, s_2) = b\sigma x_1 \dots x_{arity(\sigma)+X} \text{ avec } x_j = \begin{cases} arg_j(\sigma) & \text{si } 1 \le j \le \text{arity}(\sigma) \\ s_1 & \text{si } j = \text{arity}(\sigma) + i \\ s_2 & \text{sinon} \end{cases} $$

$$ * update_{same}(\sigma, b\sigma, s) = b\sigma x_1 \dots x_{arity(\sigma)+X} \text{ avec } x_j = \begin{cases} arg_j(\sigma) & \text{si } 1 \le j \le \text{arity}(\sigma) \\ s & \text{sinon} \end{cases} $$

<caption>FIGURE 11 – Variante de l'encodage de Viry</caption>

### 7.2.3 Extension de l'encodage à l'attribut *owise*

Une manière plus succincte d'écrire l'exemple précédent est d'utiliser l'attribut *owise* :

rule max X Y => Y requires X <Int Y
rule max X Y => X [owise]

Malheureusement, $\mathbb{K}$ ne génère pas la condition complémentaire dans le fichier KORE. Pour en-coder cet attribut, deux possibilités s'offrent à nous : implémenter un algorithme qui détermine la condition complémentaire ou considérer que toutes les conditions se réduisent nécessairement soit à true, soit à false. Comme nous ne connaissons pas exactement l'expressivité des conditions pouvant être écrites dans $\mathbb{K}$, outre qu'elles sont de type *Bool*, nous préférons ajouter l'hypothèse suivante : toute fonction construisant un booléen est une fonction totale. Sous cette hypothèse, nous pouvons générer la règle présentée en 5.(c) (Figure 11).

De plus, $\mathbb{K}$ accepte un ensemble de règles non conditionnelles avec au moins une règle ayant l'attribut *owise*. Nous excluons ce cas car nous ne pouvons pas modéliser $\ll$ Si aucune autre règle ne s'applique $\gg$, avec une condition booléenne. Cela est équivalent à l'utilisation de l'attribut *priority*($nb$), que nous ne traitons pas encore actuellement.
## 7.3 Traduction des stratégies d'évaluation

Comme nous l'avons vu à la section 6.2, il est possible que lors de la traduction de K vers KORE, des règles de réécriture conditionnelles soient générées, comme c'est le cas pour les stratégies d'évaluation définies par les attributs strict et seqstrict. Les règles de réécriture générées par ces attributs nécessitent de traduire les K computations, c'est-à-dire les symboles $\cdot$ et $\cap$, les freezers mais aussi le prédicat isKResult. L'encodage de ces différents symboles ne pose donc aucune difficulté puisque les règles présentées à la figure 10 pour les symboles s'appliquent aisément. Cependant, ces règles de réécriture conditionnelles s'inscrivent dans un cas de figure connu où l'encodage de Viry n'est pas confluent, notamment car l'ordre d'application de certaines règles de réécriture modifie le résultat de la condition, ce qui peut bloquer le calcul. En effet, la figure 12 montre, à droite, la traduction dans DEDUKTI des règles rule $E_1$ and $E_2$ $\Rightarrow E_1 \cap (\*^1_{\text{and}} E_2)$ requires $E_1 \notin KResult$ (règle C) et rule $E_1 \cap (\*^1_{\text{and}} E_2)$ $\Rightarrow E_1$ and $E_2$ requires $E_1 \in KResult$ (règle H), générées par l'attribut strict(1), et, à gauche, un exemple d'exécution valide mais bloquée$^{10}$.

<figure><img src="image_6.png" /><figcaption>FIGURE 12 – Règles générées avec l'encodage précédent et une exécution bloquée</figcaption></figure>

Intuitivement, ces règles servent à s'assurer que $E_1$ est bien d'un certain type, afin d'autoriser ou non son évaluation. L'idée de notre nouvel encodage est de spécialiser les termes de gauche des règles, c'est-à-dire d'affiner le pattern-matching afin d'assurer le type souhaité pour $E_1$. Les axiomes de sous-typage générés lors de la traduction de K vers KORE nous permettent de connaître la valeur booléenne de isKResult $E_1$ afin d'affiner correctement le pattern-matching. Nous n'appliquons donc plus notre encodage basé sur Viry dans ce cas de figure, puisque les conditions initiales deviennent inutiles.

Nous illustrons ce nouvel encodage sur l'exemple précédent.

La règle H est compilée en une règle de réécriture non conditionnelle en spécialisant le terme gauche en un terme correspondant à un booléen, soit rule (inj{Bool}{KItem} $E1) \cap (\*^1_{\text{and}} $E2) $\cap$ $c \leftrightarrow$ (inj{Bool}{BExp} $E1) \text{ and } $E2 $\cap$ $c$. Ainsi la règle H ne pourra être utilisée que si le terme est bien une expression booléenne complètement calculée. Pour la règle qui demande l'évaluation de la première expression, la règle C, nous appliquons le même principe et compilons cette règle non conditionnelle en autant de règles conditionnelles qu'il y a de cas possibles dans la sorte BExp, le cas de la constante excepté, soit :

1. rule ($X1$ and $X2$) and $E2 \cap$ $c \leftrightarrow$ ($X1$ and $X2$) $\cap$ ($\*^1_{\text{and}}$ $E2$) $\cap$ $c$

2. rule ($X1 < X2$) and $E2 \cap$ $c \leftrightarrow$ ($X1 < X2$) $\cap$ ($\*^1_{\text{and}}$ $E2$) $\cap$ $c$

3. rule (not $X1$) and $E2 \cap$ $c \leftrightarrow$ (not $X1$) $\cap$ ($\*^1_{\text{and}}$ $E2$) $\cap$ $c$

Nous ne donnons pas de formalisation de cette traduction, faute de place, mais l'exemple détaillé ci-dessus s'adapte aux autres cas présentés à la figure 9, et la généralisation est aisée.

<footnote n="10">10. Il est également possible d'obtenir false.</footnote>
# 8 Conclusion

Dans cet article, nous nous sommes principalement intéressés à la traduction dans DEDUKTI de sémantiques écrites en K, afin de pouvoir exécuter dans DEDUKTI des programmes écrits dans le langage décrit par la sémantique. Nous nous sommes appuyés sur le format KORE, sans chercher à le certifier. Nous supposons donc que le fichier KORE produit depuis une sémantique K est correcte. Ce travail a nécessité la compréhension de la traduction d'une sémantique K dans une théorie de la MATCHING LOGIC, nommée KORE, mais également de pouvoir traduire des règles conditionnelles en règles non conditionnelles. Dans l'état actuel, le traducteur KAMELO traduit la syntaxe du langage, les configurations et les symboles, certains attributs et les règles de réécriture.

Cependant, K autorise une forme restreinte de réécriture modulo ACUI, à l'aide des attributs `assoc`, `comm`, `unit` et `idem`. Dans la bibliothèque standard de K, de très rares symboles ont l'un de ces attributs, comme les dictionnaires (`Map`) et les ensembles (`Set`). A l'heure actuelle, afin de pouvoir exécuter un programme écrit dans le langage de IMP, nous avons utilisé une implantation plus classique des dictionnaires qui n'utilise pas cette fonctionnalité, et ainsi modifié très légèrement la sémantique initiale<fnref n="11" />, comme le montre la figure 13.

<table><caption>FIGURE 13 – Nouvelle sémantique de notre langage IMP</caption><thead><tr><th>IMPLÉMENTATION DES DICTIONNAIRES</th><th>MODIFICATION DE LA SÉMANTIQUE</th><th>n°</th></tr></thead><tbody><tr><td><pre>syntax Dico ::= ".Dico"<br>| "(" KItem "|--" KItem ")" "," Dico</pre></td><td></td><td></td></tr><tr><td><pre>syntax KItem ::= "lookup" KItem Dico<br>rule lookup x ((y |--> -), d) =&gt; lookup x d requires x &ne; y<br>rule lookup x ((y |--> i), -) =&gt; i requires x = y</pre></td><td><pre>rule &lt;&lt; (x &cap; s)k &lt; (d)env &gt;=&gt;<br>&lt;&lt; lookup x d &cap; s)k &lt; (d)env &gt;</pre></td><td>1'</td></tr><tr><td><pre>syntax Dico ::= "update" KItem KItem Dico<br>rule update x v ((y |--> w), d)<br>&gt;= ((y |--> w), (update x v d)) requires x &ne; y<br>rule update x v ((y |--> -), d)<br>&gt;= ((y |--> v), d) requires x = y</pre></td><td><pre>rule &lt;&lt; (x = i; &cap; s)k &lt; (d)env &gt;=&gt;<br>&lt;&lt; s)k &lt; (update x i d)env &gt;</pre></td><td>10'</td></tr><tr><td><pre>syntax Bool ::= KItem "in.dico" "(" Dico ")"<br>rule x in.dico ((y |--> -), d) =&gt; x in.dico(d) requires x &ne; y<br>rule x in.dico ((y |--> -), -) =&gt; true requires x = y<br>rule _ in.dico (.Dico) =&gt; false</pre></td><td><pre>rule &lt;&lt; (var x, xl; s)k &lt; (d)env &gt;=&gt;<br>&lt;&lt; var xl; s)k &lt; ((x |--> 0), d)env &gt;<br>requires not Bool (x in.dico(d))</pre></td><td>16'</td></tr></tbody></table>

Notre outil ne peut donc pas traiter actuellement les sémantiques faisant usage de la réécriture modulo ACUI. Nous avons également supposé que les variables du membre droit d'une règle de réécriture K apparaissent nécessairement dans le membre gauche, ce qui est une restriction très commune en théorie de la réécriture. Cependant cette hypothèse est invalidée par la sémantique K du langage Michelson [8]. La perspective la plus immédiate de ce premier travail consiste à étendre l'outil KAMELO de manière à prendre en considération les attributs tels que `priority`(*nb*) et à mener une expérimentation sur une collection de sémantiques écrites avec K. Nous comptons également étendre notre transformation d'un CTRS vers un TRS afin de pouvoir garantir la correction et la compléture de celle-ci, en plus de la préservation de la terminaison et de la confluence. Un autre travail futur concerne la réécriture modulo ACUI que nous contournons actuellement. Une piste ici consiste à mettre en place un encodage *ad hoc* de manière à pouvoir utiliser les dictionnaires et les ensembles tels qu'ils sont implantés dans la bibliothèque de K.

**Remerciements** : Nous remercions vivement l'équipe K, notamment XIAOHONG CHEN, EVETT HILDENBRANDT, ZHENGYAO LIN et DOREL LUCANU, pour les réponses rapides à nos multiples questions.

<footnote n="11">11. Comme les chaînes de caractères ne sont pas natives dans DEDUKTI, nous considérons qu'une variable est de la forme `var`(*nb*). L'égalité sur les identifiants des variables revient donc à une égalité sur les entiers.</footnote>
Bibliographie

[1] GitHub avec la formalisation de K en K. https://github.com/kframework/k-in-k.

[2] GitHub de Dedukti. https://github.com/Deducteam/Dedukti.

[3] GitHub de Dedukti v3. https://github.com/Deducteam/lambdapi.

[4] GitLab de KaMeLo. https://gitlab.com/semantiko/kamelo.

[5] Site web de l'école d'été ISR 2021. https://dalila.sip.ucm.es/isr2021/.

[6] Site web de K. https://kframework.org/.

[7] Site web de Sail. https://www.cl.cam.ac.uk/~pes20/sail/.

[8] Sémantique K de Michelson. https://github.com/runtimeverification/michelson-semantics.

[9] A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek, C. Dubois, F. Gilbert, P. Halmagrand, O. Hermant, and R. Saillard. Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system. In *TYPES : Types for Proofs and Programs*, Novi SAd, Serbia, May 2016.

[10] F. Blanqui, G. Dowek, E. Grienenberger, G. Hondet, and F. Thiré. Some Axioms for Mathematics. In N. Kobayashi, editor, *6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)*, volume 195 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 20:1–20:19, Dagstuhl, Germany, 2021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.

[11] D. Bogdănăsă and G. Roșu. K-Java : A Complete Semantics of Java. In *Proceedings of the 42nd Symposium on Principles of Programming Languages (POPL'15)*, pages 445–456. ACM, January 2015.

[12] P. Borras, D. Clement, T. Despeyroux, J. Bertot, G. Kahn, B. Lang, and V. Pascual. Centaur : The system. 24:14–24, 03 1989.

[13] X. Chen, Z. Lin, M.-T. Trinh, and G. Roșu. Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. In *Proceedings of the 33rd International Conference on Computer-Aided Verification*. ACM, July 2021.

[14] X. Chen, D. Lucanu, and G. Roșu. Matching Logic Explained. Technical Report http://hdl.handle.net/2142/107794, University of Illinois at Urbana-Champaign and Alexandru Ioan Cuza University, July 2020.

[15] X. Chen and G. Roșu. Applicative Matching Logic : Semantics of K. Technical Report http://hdl.handle.net/2142/104616, University of Illinois at Urbana-Champaign, July 2019.

[16] X. Chen and G. Roșu. Matching mu-Logic : Foundation of K Framework (Invited Paper). page 4 pages, 2019. Artwork Size : 4 pages Medium : application/pdf Publisher : Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany Version Number : 1.0.

[17] D. Cousineau and G. Dowek. Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo. In *TLCA*, 2007.

[18] N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In *Handbook of Theoretical Computer Science, Volume B : Formal Models and Semantics*, pages 243–320, 1990.

[19] G. Dowek. Interacting Safely with an Unsafe Environment. CoRR, abs/2107.07662, 2021.

[20] C. Hathhorn, C. Ellison, and G. Roșu. Defining the Undefinedness of C. In *Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15)*, pages 336–345. ACM, June 2015.

[21] L. Li and E. L. Gunter. IsaK-static : A complete static semantics of K. In *Formal Aspects of Component Software - 15th International Conference, FACS 2018, Proceedings*, pages 196–215. Springer-Verlag Berlin Heidelberg, 2018.

[22] L. Li and E. L. Gunter. A Complete Semantics of K and Its Translation to Isabelle. In A. Cerone and P. C. Ölveczky, editors, *Theoretical Aspects of Computing – ICTAC 2021*, pages 152–171, Cham, 2021. Springer International Publishing.

[23] D. Mulligan, S. Owens, K. Gray, T. Ridge, and P. Sewell. Lem : Reusable Engineering of Real-world Semantics. *ACM SIGPLAN Notices*, 49, 08 2014.
[24] D. Park, A. Ştefănescu, and G. Roşu. KJS : A Complete Formal Semantics of JavaScript. In *Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15)*, pages 346–356. ACM, June 2015.

[25] G. Roşu. K - A Semantic Framework for Programming Languages and Formal Analysis Tools. In D. Peled and A. Pretschner, editors, *Dependable Software Systems Engineering*, NATO Science for Peace and Security. IOS Press, 2017. From the lecture notes presented at Marktoberdorf'16.

[26] G. Roşu and T. F. Şerbănută. An overview of the K semantic framework. *The Journal of Logic and Algebraic Programming*, 79(6):397–434, Aug. 2010.

[27] P. Sewell, F. Z. Nardelli, S. Owens, G. Peskine, T. Ridge, S. Sarkar, and R. Strniša. Ott: Effective tool support for the working semanticist. *Journal of Functional Programming*, 20(1):71–122, 2010.

[28] A. Stefănescu, D. Park, S. Yuwen, Y. Li, and G. Roşu. Semantics-based program verifiers for all languages. In *Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications*, pages 74–91, Amsterdam Netherlands, Oct. 2016. ACM.

[29] M. G. J. van den Brand, A. van Deursen, J. Heering, H. A. de Jong, M. de Jonge, T. Kuipers, P. Klint, L. Moonen, P. A. Olivier, J. Scheerder, J. J. Vinju, E. Visser, and J. Visser. The Asf+Sdf Meta-environment : A Component-Based Language Development Environment. In R. Wilhelm, editor, *Compiler Construction*, pages 365–370, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg.

[30] P. Viry. Elimination of Conditions. *Journal of Symbolic Computation*, 28(3):381–401, 1999.