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

HAL
open science

# A Meta-Approach to Describe Effectful and Distributed Semantics

Adam Khayam

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

## To cite this version:

Adam Khayam. A Meta-Approach to Describe Effectful and Distributed Semantics. Computer Vision and Pattern Recognition [cs.CV]. Université Rennes 1, 2022. English. NNT: 2022REN1S070. tel-03969183v3

HAL Id: tel-03969183

https://theses.hal.science/tel-03969183v3

Submitted on 2 Feb 2023

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_3.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
UNIVERSITÉ DE

RENNES 1

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

THÈSE DE DOCTORAT DE

L'UNIVERSITÉ DE RENNES 1

ÉCOLE DOCTORALE N° 601

Mathématiques et Sciences et Technologies
de l'Information et de la Communication

Spécialité : Informatique

Par

Adam KHAYAM

A Meta-Approach to Describe Effectful and Distributed Semantics

Thèse présentée et soutenue à Salle Métivier (C024), INRIA Rennes, le 30/11/2022

Unité de recherche : CELTIQUE/EPICURE

**Rapporteurs avant soutenance :**

Catherine DUBOIS Professeure, Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise

Sukyoung RYU Professeure, Korea Advanced Institute of Science and Technology

**Composition du Jury :**

Attention, en cas d'absence d'un des membres du Jury le jour de la soutenance, la composition du jury doit être revue pour s'assurer qu'elle est conforme et devra être répercutée sur la couverture de thèse

Président : Sandrine BLAZY

Professeure Université de Rennes 1

Examinateurs : Xavier RIVAL

Directeur de Recherche, INRIA Paris

Arthur CHARGUÉRAUD Chargé de Recherche, INRIA Nancy

Dir. de thèse : Alan SCHMITT

Directeur de Recherche, INRIA Rennes

Co-dir. de thèse : Tamara REZK

Directrice de Recherche, INRIA Sophia Antipolis
<figure><img src="image_5.png" /></figure>
ACKNOWLEDGEMENT

Another experience has finished, and I am thankful to the universe for that. It seems
yesterday that I started my doctoral path, and now it is its end.

First, I would like to thank the reviewers that have carefully read my thesis and given
insightful comments. It is such a heavy document, so I can only thank you for your time
reading and commenting on it. In the same way, I would like to thank the rest of the jury:
time is valuable, and dedicating your time to me means a lot.

Now let's talk about these three years. I had a wonderful time in Rennes, even during
the pandemic. One of the pillars of this period was my team (Celtique/Epicure). I thank
each of you, I loved everything, but I am a fan of the small things. For example, at the
pandemic's beginning, you organized "la pause café" to chat each afternoon. It was a
sparkle of normality. I have a lot of respect for you, and I could not have been luckier.
The Celtique/Epicure team is amazing.

A special mention goes to my friends in Rennes. We had a wonderful time during a
crazy period. We were a stronghold to each other, and we made that crisis one of the best
parts of our lives. I wanted to cite each one of you and your papers. A material way to
thank you individually, but suddenly I realized you already have too many citations :p.

I want to thank also my colleagues in Sophia Antipolis, my friends in Nice, and the
people that often visit from Paris. I always found a great environment there and felt
welcomed by both the teams on the floor, INDES and STAMP.

Then, let's talk about my parents in academia, Alan and Tamara, ladies first. Thank
you for hiring me; I hope I did not disappoint you. I learned a lot from you, and I am
always thankful for your belief in me. Alan, it was quite an adventure. I came to you as
a profane, and you had the patience and ability to introduce me to the topic. You helped
me a lot with your knowledge and your personality. Whenever I was insecure about what
to do, I knew that I had you covering my back.

I am lucky. I couldn't have hoped for a better academic family.

Let's go to my biological family. I thank you for your patience, mostly when I don't
pick up the phone and answer back. I love you!

Last but not least: Moudy, nothing would have started without you. Thank you,
brother!
<figure><img src="image_6.png" /></figure>

**Titre** : Une Méta-Approche pour Décrire des Sémantiques avec Effets et Distribuée

**Mot clés** : Sémantique Squelettique ; Langage de Spécification ; ECMAScript ; Monades ; Systèmes Distribués ; Internet des Objets

**Résumé** : L'étude de la sémantique des langages de programmation est un domaine de l'informatique visant à représenter formellement le comportement de programmes. L'état de l'art a beaucoup progressé au cours des quatre dernières décennies en proposant de plus en plus de cadres adaptés à la réalisation de ces études. S'il existe de nombreux styles, dont on connaît les caractéristiques positives et les limites, il reste encore beaucoup à faire en termes d'outils adaptés à la description et à l'étude de la sémantique des langages de programmation.

Cette thèse s'inscrit dans ce contexte, en proposant une méthodologie pour pouvoir produire un objet représentant le comportement d'un langage de programmation, en fournissant tout ce qui est nécessaire pour pouvoir les étudier. La contribution de la thèse consiste à fournir une méthodologie pour écrire une sémantique concise et visuellement proche d'une spécification. Pour ce faire, nous utilisons un certain nombre de constructions algébriques qui, associées à notre approche purement fonctionnelle, conduisent à

une formalisation claire, concise et facile à maintenir. Nous avons appliqué cette technique à deux études de cas, la modélisation de la spécification JavaScript, ECMAScript, et la représentation d'un modèle formel pour décrire la sémantique d'orchestration représentant le comportement des applications de l'internet des Objets. Ces travaux donnent une idée claire du potentiel et de l'expressivité de notre cadre formel, appelé sémantique squelettique [8, 41].

Ce manuscrit est à la fois une introduction à l'utilisation de la sémantique squelettique et son application aux langages de programmation, même quand ceux-ci ont une spécification complexe et de taille conséquente. C'est également une étude de la manière d'exploiter les caractéristiques d'un tel outil pour produire des formalisations qui peuvent être claires et lisibles par l'homme. En substance, il s'agit de faire d'une représentation mathématique d'un langage, qui s'adresse à une catégorie spécifique de chercheurs, un support précieux pour les programmeurs en vue d'implémentations réelles.
<figure><img src="image_7.png" /></figure>

**Title:** A Meta-Approach to Describe Effectful and Distributed Semantics

**Keywords:** Skeletal Semantics; Specification Language; ECMAScript; Monads; Distributed Systems; Internet of Things

**Abstract:** The study and production of programming language semantics is a computer science field aiming to represent these objects' behavior formally. The State-of-the-art presents different styles and technologies for working on semantics. Technologies have progressed a lot during the last four decades by proposing more and more frameworks adapted to carry out these studies. On the one hand, semantic styles have well-known positive characteristics and limitations. On the other hand, semantic tools are an active research topic.

The thesis proposes a methodology for encoding semantics in a tiny functional meta-language called Skel [41]. This language has a suite of tools for generating different artefacts for performing different types of studies. The methodology proposed in this thesis shows how to write concise semantics visually close to a programming language specifica-

tion. To do so, we combined different algebraic constructs for writing precise, concise, readable, and easily maintainable formalizations. We have applied this technique to two case studies, the modeling of the JavaScript specification, ECMAScript, and the representation of a formal model to describe orchestration semantics representing the behavior of Internet of Things applications. These works give a clear idea of the potential and expressiveness of our formal framework—Skeletal Semantics [8].

This manuscript is an introduction to Skeletal Semantics, showing how to produce usable and human-readable formalizations of different types of specifications—inference-rule based and in prose. In essence, the aim is to turn a mathematical representation of a language addressed to a specific category of researchers into valuable support for programmers to build real implementations.
RÉSUMÉ EN FRANÇAIS

Tout langage de programmation peut être considéré comme un ensemble de règles (sémantique) représentant le comportement de ses éléments atomiques (syntaxe). Compte tenu certaines données (entrées) et d'une instance syntaxique d'un langage de programmation (programme), une interprétation est un processus permettant de renvoyer un résultat (sortie) en transformant les données par des manipulations du programme effectuées conformément aux règles du langage.

Un parallèle légitime peut être fait avec les langues naturelles. En effet, si avec une langue naturelle on construit des discours, interprétables par les interlocuteurs, avec les langages de programmation on produit des programmes, des directives pour la machine. Pour comprendre ces directives, il faut disposer d'un programme qui interprète le programme à la machine. Ce dernier doit être clair et sans ambiguïté, car l'interprétation du programme nécessite une représentation de la syntaxe et la sémantique dans laquelle ce programme est écrit.

Dans ce manuscrit, nous traitons de différents types de sémantique des langages de programmation et de leur représentation. Plus précisément, nous proposons un moyen efficace de représenter la sémantique des langages de programmation d'une manière qui soit concise et fidèle aux spécifications qui représentent leur comportement. Ces langages peuvent être de nature différente, tendant à être définis, de manière informelle, en langage naturel ou pseudo-algorithmique, ou, de manière formelle, en notation mathématique. Dans cette thèse, nous montrerons que, grâce à un petit méta langage appelé Skel, nous sommes capables de capturer la sémantique de ces deux types de spécifications. De ces définitions formelles, on extrait ensuite du code pour pouvoir produire de manière modulaire un interpréteur sur lequel on peut exécuter des programmes.
# Définition de Langages Dans la Sémantique Squelettique.

Pour représenter formellement la définition d'un langage de programmation, il est généralement nécessaire de définir la syntaxe et la sémantique des constructions du langage.

Par exemple, si nous devions considérer un langage de programmation qui ne fait que des additions d'entiers, nous pourrions définir sa syntaxe de la manière suivante.

$$VALUE \ v ::= n$$

$$EXPR \ e ::= v | e_1 + e_2$$

Avec cette représentation, on dit que les valeurs du langage sont les entiers, qui dans ce cas n'ont pas de définition réelle, et qu'une expression du langage est soit une valeur, soit une somme entre deux expressions.

En ce qui concerne la sémantique des expressions dans ce langage, il existe les différents formalismes qui peuvent être utilisés. Dans cette thèse, nous nous limiterons à sémantique opérationnelle, un cadre logique qui sert à décrire comment une construction de la langue est exécutée. Dans ce qui suit, nous présentons la sémantique du petit exemple de syntaxe défini ci-dessus.

$$\frac{\text{VALEUR}}{n \Downarrow e n} \qquad \frac{\text{ADDITION}}{e_1 \Downarrow n_1 \qquad e_2 \Downarrow n_2}$$

La première règle, Valeur, renvoie un nombre entier dans le cas où l'expression est simplement une valeur de la langue. La deuxième règle, Addition, évalue l'addition. Dans le cas d'une somme, il évalue le premier terme de l'addition, le second, et renvoie la somme des deux entiers. Comme la définition d'une expression est récursive, cette règle simple évalue également les sommes qui comportent d'autres additions entre des entiers en tant que sous-expressions. Dans la thèse, nous écrirons la plupart de la sémantique en utilisant la sémantique squelettique [8].

Pour donner immédiatement un aperçu de la puissance de la sémantique squelettique et du Skel, il faut considérer la conclusion de la règle, $n_1 + n_2$. Comme les entiers, l'addition n'a pas non plus de définition réelle, autre que celle que nous pourrions naturellement lui donner. Le langage Skel, est un petit langage fonctionnel défini
pour l'écriture de la sémantique. Exactement comme la définition formelle de ce langage avec l'addition, nous pouvons définir ce langage en Skel, avec le même niveau d'abstraction. Ce langage décrit la règle, et non le programme qui la représente.

```pascal
type int

type value = | Int int
type expression = | Val value | Plus (expression, expression)

val plus : expression -> expression -> int

val eval (e:expression) : nat =
  branch let Val (Int n) = e in n
  or
  let Add (e_1, e_2) = e in
  let n_1 = eval e_1 in
  let n_2 = eval e_2 in
  plus n_1 n_2
end
```

En fait, en regardant le code, nous pouvons voir que nous définissons trois types, un pour les entiers, un pour les valeurs et un pour les expressions, mais contrairement aux deux derniers, les entiers, `type int`, n'ont pas de définition. Il en va de même pour l'addition `val plus`. Cette opération ne définit pas l'algorithme de la somme, elle indique simplement qu'il existe un terme qui prend deux entiers et renvoie un entier. Quant à la fonction `eval`, dans le cas où l'expression est une valeur, elle renvoie l'entier qu'elle encapsule, sinon, pour la somme, elle évalue la première expression, la seconde, et enfin renvoie la somme des deux entiers.

En général, pour des langages aussi petits, il est indifférent d'écrire la sémantique d'un langage de programmation sur papier ou sur une machine. Le problème se pose lorsque les langues sont de grande taille. En fait, certifier une grande sémantique sur le papier est presque impossible, ne serait-ce qu'en raison de la quantité de notation qui doit être définie afin d'avoir des formalisations compactes. Il ne faut pas non plus oublier que la démonstration par induction sur des définitions de langages aussi larges sur papier est compliquée. Au cours des dernières décennies, différentes approches ont été portées à l'état de l'art dans le but de pouvoir écrire la sémantique sur une machine, et de pouvoir utiliser le support de la machine pour certifier les inter-
prètes résultants. Il existe deux philosophies : l'une impliquant l'utilisation d'assistants de démonstration tels que Coq [70], HOL [29], Isabelle [30], Twelf [71, 27], et l'autre exploitant les logiciels et les environnements définis pour écrire la sémantique, tels que K [63], Ott [66], Lem [55], PLT [36]. La langue Skel est placée dans la deuxième catégorie. Contrairement aux concurrents de la deuxième catégorie, avec Skel on ne peut pas exécuter directement des programmes, mais on peut générer divers artefacts grâce à l'ensemble des outils fournis par necro [53].

Nous aborderons les styles et outils sémantiques dans la première partie de cette thèse.

Dans les parties 2 et 3, nous montrerons comment exploiter ce langage pour écrire des sémantiques pour des langages au comportement complexe.

## Contributions

Les contributions de la thèse sont présentées dans les deuxième et troisième parties.

Dans la deuxième partie, les contributions sont de décrire une approche systématique pour écrire la sémantique d'une manière concise qui est fidèle à sa spécification, facilement maintenable, et à partir de laquelle un interprète peut être généré pour exécuter des programmes. Les langages que nous allons considérer ont des effets secondaires, tels que la modification de la mémoire, la présence d'exceptions, et suspensions du code. Dans cette partie de la thèse, nous présenterons d'abord une série de langages jouets et leur formalisation en Skel. Ces langages seront une extension de l'autre, et leur formalisation restera structurellement la même, déléguant la propagation des effets secondaires aux opérateurs monadiques. Nous présenterons plus tard la mécanisation d'ECMAScript. Nous utiliserons le même modus operandi pour produire une description formelle structurellement solide de cette spécification. La contribution dans ce cas est une formalisation concise, maintenable et lisible de la sémantique de l'ECMAScript; la génération d'un interpréteur fonctionnel et l'exécution de petits programmes.

Dans la troisième partie de la thèse, la contribution consiste à raffiner une sémantique déjà existante représentant le comportement d'un système distribué particulier. En fait, le contexte de ce système est celui des applications web qui incluent des interactions avec des dispositifs connectés au réseau. Nous appelons généralement ces systèmes *Internet des Objets* (IoT). Une autre contribution de cette partie est
la production d'un interprète pour cette sémantique, montrant que ce modèle formel non-déterministe pose des problèmes lors de son exécution, car il est complexe. Une dernière contribution de cette partie est la définition d'un ordonnanceur pour ce modèle qui limite le non-déterminisme, rendant le modèle exécutable. Pour soutenir la correc- tion de l'ordonnanceur, nous fournirons un théorème d'équivalence entre la séman- tique non-déterministe et celle de l'ordonnanceur.

Les contributions de la deuxième partie de la thèse sont présentées dans deux articles publiés et un en cours de révision [34, 33, 35].

Les contributions de la troisième partie de la thèse sont actuellement en cours de rédaction sous forme d'article.

# Plan du Manuscrit

La thèse se compose de trois parties.

Le premier présentera, dans le chapitre 1, les techniques standard pour représenter formellement le comportement des constructions linguistiques d'un langage de pro- grammation, et dans le chapitre 2, les logiciels créés pour avoir une représentation formelle de ces langages sur une machine. En détail, ce dernier chapitre présentera la sémantique des squelettes et le langage Skel, un petit langage fonctionnel permettant d'écrire des spécifications de langage.

La deuxième partie de la thèse traitera de la manière de capturer les effets sec- ondaires des spécifications du langage. Par exemple, les langages peuvent avoir un état modifié, gérer les exceptions, suspendre l'exécution de certains segments de code. Ces effets sont généralement peu pratiques à gérer, car ils doivent être représen- tés explicitement dans un langage purement fonctionnel.

Dans le chapitre 3, nous verrons comment définir de manière modulaire la séman- tique d'un petit langage de programmation jouet, que nous étendrons progressivement en introduisant de nouvelles constructions de langage et des effets secondaires. Nous montrerons que grâce à l'utilisation des monades, nous serons en mesure d'écrire des représentations extrêmement modulaires, solides et facilement extensibles en Skel. La propagation des effets secondaires sera gérée, implicitement, par les opérateurs monadiques.

Dans le chapitre 4, nous utiliserons les techniques d'écriture sémantique définies dans le chapitre précédent pour représenter la sémantique d'un langage réel, JavaScript.
Contrairement au chapitre précédent, où les spécifications du langage étaient décrites par des règles d'inférence logique, dans ce chapitre nous nous baserons sur une spécification textuelle. Contrairement à d'autres langages, comme Python, la spécification de JavaScript est extrêmement précise. Nous montrerons que notre technique d'écriture parvient à capturer, de manière fidèle, concise et maintenable, le comportement du langage. A partir de la représentation formelle, nous allons générer un interpréteur de noyau JavaScript et montrer l'exécution d'un petit programme. Pouvoir représenter l'ensemble de la spécification est utopique, en fait notre principale contribution est de montrer que le langage est suffisamment expressif pour rendre cette tâche historiquement difficile relativement simple.

La troisième partie de ce document présentera, au chapitre 5, une sémantique représentant le comportement d'un système distribué. Ce modèle, cherche à exprimer l'évolution de ces systèmes dans le contexte de l'Internet des objets. Nous allons montrer la sémantique, d'abord à travers les règles d'inférence et ensuite en Skel. Nous discuterons de la lourdeur de l'exécution de ce modèle, qui est non-déterministe par nature, et présenterons une solution, un ordonnanceur qui tentera de limiter le non-déterminisme inhérent à ce modèle. Nous montrerons que la sémantique du l'ordonnanceur est équivalente à la sémantique non-déterministe, ce qui rend possible l'exécution de programmes exécutés sur ce modèle, quelle que soit la complexité du programme.
# TABLE OF CONTENTS

## Introduction 2

## I Background 5

### 1 Semantic Styles 7

1.1 A While Language 8

1.2 Operational Semantics 10

1.2.1 Structural Operational Semantics 11

1.2.2 Big-Step Operational Semantics 15

1.3 Abstract Machines 18

1.4 Pretty-Big-Step Semantics 21

### 2 The Skel Specification Language 27

2.1 The Skel Language 28

2.1.1 An Arithmetic Language in Skel 29

2.1.1.1 Syntax and Semantics 29

2.1.2 The Necro Ecosystem 32

2.1.3 An Interpreter for The Arithmetic Language 36

2.2 Related Specification Language 39

2.3 Conclusion 41

## II Effectful Semantics 43

### 3 Describing Concisely Effectful Semantics 45

3.1 Effectful Arithmetic Language 47

3.2 PCF 54

3.3 Adding State to the PCF language 59

3.4 A Fully Monadic Skeletal Semantics 64

3.5 Explicit Contination Manipulation 69
<table><tr><td>3.5.1 Program Examples</td><td>70</td></tr><tr><td>3.5.2 Syntax and Semantics</td><td>71</td></tr><tr><td>3.5.3 A Stateful PCF Language with Yield and Exceptions in Skel</td><td>77</td></tr><tr><td>3.6 Related Work</td><td>81</td></tr><tr><td><b>4 A Faithful Description of ECMAScript in Skeletal Semantics</b></td><td><b>85</b></td></tr><tr><td>4.1 ECMAScript Algorithms in Skel</td><td>87</td></tr><tr><td>4.1.1 ECMAScript</td><td>87</td></tr><tr><td>4.1.2 Challenges of the Formalization</td><td>88</td></tr><tr><td>4.1.3 Completion Record and the ECMAScript Error Handling (?) monad</td><td>97</td></tr><tr><td>4.1.4 A Control-Flow monad</td><td>100</td></tr><tr><td>4.1.5 A Real Example in Skel</td><td>103</td></tr><tr><td>4.1.6 Current Status</td><td>106</td></tr><tr><td>4.2 Interpreter Evaluation</td><td>109</td></tr><tr><td>4.2.1 Interpreter Instantiation</td><td>109</td></tr><tr><td>4.2.2 Evaluation</td><td>110</td></tr><tr><td>4.2.2.1 Framework Comparison</td><td>110</td></tr><tr><td>4.2.2.2 Program Execution</td><td>112</td></tr><tr><td>4.3 Related Work</td><td>113</td></tr></table>

## III Distributed Semantics 117

<table><tr><td><b>5 An Executable Semantics for Distributed IoT Applications</b></td><td><b>119</b></td></tr><tr><td>5.1 Context</td><td>121</td></tr><tr><td>5.2 WEBI: A Formal Semantics to IoT Applications</td><td>123</td></tr><tr><td>5.2.1 The WEBI Configuration</td><td>123</td></tr><tr><td>5.2.2 Semantics</td><td>127</td></tr><tr><td>5.2.2.1 WEBI Transition Relation</td><td>129</td></tr><tr><td>5.2.2.2 Client-Driven Rules</td><td>129</td></tr><tr><td>5.2.2.3 Service-Driven Rules</td><td>135</td></tr><tr><td>5.2.2.4 Device-driven Rules</td><td>138</td></tr><tr><td>5.2.2.5 The Evaluation Function</td><td>142</td></tr><tr><td>5.2.3 Example: The Cost of Non-Determinism</td><td>145</td></tr><tr><td>5.2.3.1 Initial WEBI Configuration Setting</td><td>146</td></tr></table>
<table><tr><td>5.2.3.2</td><td>Execution</td><td>152</td></tr><tr><td>5.3</td><td>A Scheduler for WEBI</td><td>155</td></tr><tr><td>5.3.1</td><td>Semantics</td><td>155</td></tr><tr><td>5.3.1.1</td><td>Assumptions for the Scheduler</td><td>156</td></tr><tr><td>5.3.1.2</td><td>Scheduler Configuration</td><td>159</td></tr><tr><td>5.3.1.3</td><td>Small-Step Semantics</td><td>161</td></tr><tr><td>5.3.2</td><td>Equivalence of the Scheduler and the WEBI Semantics</td><td>168</td></tr><tr><td>5.3.2.1</td><td>Commutation Lemmas</td><td>169</td></tr><tr><td>5.3.2.2</td><td>Interval Lemmas</td><td>173</td></tr><tr><td>5.3.2.3</td><td>Proof Sketch of Theorem 1</td><td>175</td></tr><tr><td>5.3.3</td><td>Executing the Example of Section 5.2.3 in Skel</td><td>177</td></tr><tr><td colspan="2">Conclusion</td><td>182</td></tr><tr><td colspan="2">Bibliography</td><td>187</td></tr></table>
<figure><img src="image_8.png" /></figure>
LIST OF FIGURES

<table><tr><td>1.1</td><td>Definition of the While language grammar.</td><td>8</td></tr><tr><td>1.2</td><td>Expression evaluation function φ</td><td>10</td></tr><tr><td>1.3</td><td>Example</td><td>10</td></tr><tr><td>1.4</td><td>Small-Step expression evaluation. This description matches the behavior defined in Figure 1.2.</td><td>12</td></tr><tr><td>1.5</td><td>Small-Step commands evaluation.</td><td>13</td></tr><tr><td>1.6</td><td>Commands Evaluation in Big-Step</td><td>16</td></tr><tr><td>1.7</td><td>First level of the big-step derivation tree of the program. We put ... when we refer to the rest of the program.</td><td>17</td></tr><tr><td>1.8</td><td>Abstract Machine definition of expression evaluation.</td><td>19</td></tr><tr><td>1.9</td><td>Abstract Machine definition of commands evaluation.</td><td>20</td></tr><tr><td>1.10</td><td>Expression Evaluation with Option Results in Big-Step</td><td>22</td></tr><tr><td>1.11</td><td>Expression Evaluation in Pretty-Big-Step.</td><td>23</td></tr><tr><td>1.12</td><td>Syntax definition of the language in Pretty-Big-Step style.</td><td>24</td></tr><tr><td>1.13</td><td>Commands Evaluation in Pretty-Big-Step</td><td>25</td></tr><tr><td>2.1</td><td>skeleton for the While constructor</td><td>28</td></tr><tr><td>2.2</td><td>Arithmetic Language</td><td>30</td></tr><tr><td>2.3</td><td>Arithmetic Language Definition in Skel</td><td>31</td></tr><tr><td>2.4</td><td>The Necro ecosystem.</td><td>32</td></tr><tr><td>2.5</td><td>The interpretation monad module and its identity monad instantiation</td><td>34</td></tr><tr><td>2.6</td><td>The UNSPEC module type and its functors.</td><td>38</td></tr><tr><td>2.7</td><td>The INTERPRETER module type and its functor.</td><td>39</td></tr><tr><td>3.1</td><td>Syntax of the Exception type</td><td>48</td></tr><tr><td>3.2</td><td>Arithmetic Language Rules Extended with Division and Exceptions</td><td>48</td></tr><tr><td>3.3</td><td>Arithmetic Language in Skel Extended with Division and Exceptions</td><td>49</td></tr><tr><td>3.4</td><td>Exception monad in Skel, and its application to the eval function</td><td>52</td></tr><tr><td>3.5</td><td>Exception Monad and its Symbolic Application to eval</td><td>53</td></tr></table>
<table><tr><td>3.6</td><td>The zero term implementation</td><td>54</td></tr><tr><td>3.7</td><td>PCF Semantic Rules</td><td>56</td></tr><tr><td>3.8</td><td>PCF Semantics in Skel</td><td>57</td></tr><tr><td>3.9</td><td>extEnv instantiation in OCaml</td><td>58</td></tr><tr><td>3.10</td><td>PCF with References</td><td>62</td></tr><tr><td>3.11</td><td>Sample of the updated functions</td><td>66</td></tr><tr><td>3.12</td><td>Functions for creating closures. The output is a computation in the monad.</td><td>67</td></tr><tr><td>3.13</td><td>Delimited Sequence of Yield</td><td>70</td></tr><tr><td>3.14</td><td>Two Ways Communication through Yield</td><td>71</td></tr><tr><td>3.15</td><td>Abstract Machine for PCF + state + delimited continuations.</td><td>73</td></tr><tr><td>3.16</td><td>Yield Language in Skel</td><td>77</td></tr><tr><td>3.17</td><td>Ping-Pong State Updates through Yield</td><td>81</td></tr><tr><td>4.1</td><td>State Monad in Skel</td><td>89</td></tr><tr><td>4.2</td><td>Internal representation of the object {n : 42}.</td><td>96</td></tr><tr><td>4.3</td><td>Example of algorithmic steps in which a local environment is necessary.</td><td>96</td></tr><tr><td>4.4</td><td>Skel Formalization of ES Completion Records</td><td>97</td></tr><tr><td>4.5</td><td>Out and Anomaly Declarations</td><td>98</td></tr><tr><td>4.6</td><td>The Model of ? and !.</td><td>99</td></tr><tr><td>4.7</td><td>The controlFlow type with binders and setters</td><td>100</td></tr><tr><td>4.8</td><td>Code with and without Control Flow Monad.</td><td>101</td></tr><tr><td>4.9</td><td>Variant of the Figure 4.8 with Exceptions.</td><td>103</td></tr><tr><td>4.10</td><td>The ECMAScript's GetValue(V) and its Skel formalization</td><td>104</td></tr><tr><td>4.11</td><td>yieldable abstract closure</td><td>108</td></tr><tr><td>4.12</td><td>TYPES module instantiation.</td><td>109</td></tr><tr><td>4.13</td><td>GetValue 5.1 written in the K framework.</td><td>111</td></tr><tr><td>4.14</td><td>GetValue 5.1 in JSCert.</td><td>112</td></tr><tr><td>4.15</td><td>Example of JS program</td><td>113</td></tr><tr><td>5.1</td><td>The ServiceInit rule. A client is initialized. The booting call of this client generate a running web service.</td><td>130</td></tr><tr><td>5.2</td><td>ServiceInit Skel rule.</td><td>131</td></tr><tr><td>5.3</td><td>The ClientStep rule. A web client performs an evaluation step.</td><td>132</td></tr><tr><td>5.4</td><td>ClientStep Skel rule.</td><td>132</td></tr><tr><td>5.5</td><td>The ClientCall rule. A client calls a web service.</td><td>133</td></tr></table>
<table>
  <tbody>
    <tr>
      <td>5.6 ClientCall Skel rule.</td>
      <td>133</td>
    </tr>
    <tr>
      <td>5.7 The Run rule. When a client finishes to compute, it picks a chunk and executes it.</td>
      <td>134</td>
    </tr>
    <tr>
      <td>5.8 Run Skel rule.</td>
      <td>135</td>
    </tr>
    <tr>
      <td>5.9 The ServiceStep rule. A service performs an evaluation step.</td>
      <td>135</td>
    </tr>
    <tr>
      <td>5.10 ServerStep Skel rule.</td>
      <td>136</td>
    </tr>
    <tr>
      <td>5.11 The RetServiceBoot rule. A service related to a booting client finishes to compute. It returns the result to the client.</td>
      <td>137</td>
    </tr>
    <tr>
      <td>5.12 RetServiceBoot Skel rule.</td>
      <td>138</td>
    </tr>
    <tr>
      <td>5.13 The RetService rule. A service realted to a running client finishes to compute. It returns the result to the client.</td>
      <td>138</td>
    </tr>
    <tr>
      <td>5.14 RetService Skel rule.</td>
      <td>139</td>
    </tr>
    <tr>
      <td>5.15 The DeviceSensor rule. A sensor, or a group of sensors detects a physical event.</td>
      <td>139</td>
    </tr>
    <tr>
      <td>5.16 DeviceSensor Skel rule.</td>
      <td>140</td>
    </tr>
    <tr>
      <td>5.17 The DeviceActuator rule. A service issues an actuation order to a device. The device performs the actuation.</td>
      <td>140</td>
    </tr>
    <tr>
      <td>5.18 DeviceActuator Skel rule.</td>
      <td>141</td>
    </tr>
    <tr>
      <td>5.19 The DeviceReading rule. A service issues an reading order to a device. The device responds, returning a serialized value.</td>
      <td>141</td>
    </tr>
    <tr>
      <td>5.20 DeviceReading Skel rule.</td>
      <td>142</td>
    </tr>
    <tr>
      <td>5.21 The pseudo-random interpretation monad</td>
      <td>143</td>
    </tr>
    <tr>
      <td>5.22 The List interpretation monad</td>
      <td>144</td>
    </tr>
    <tr>
      <td>5.23 ServiceInit Skel rule</td>
      <td>145</td>
    </tr>
    <tr>
      <td>5.24 The windowManager service definition.</td>
      <td>147</td>
    </tr>
    <tr>
      <td>5.25 The turnOnOven service definition.</td>
      <td>147</td>
    </tr>
    <tr>
      <td>5.26 Definition of a client calling the windowManager and the _I_ set.</td>
      <td>148</td>
    </tr>
    <tr>
      <td>5.27 Type defining the device's semantics.</td>
      <td>149</td>
    </tr>
    <tr>
      <td>5.28 The window semantics. The code is written in a simplyfied version of Skel, which has, for example, strings.</td>
      <td>149</td>
    </tr>
    <tr>
      <td>5.29 The thermometer semantics and instantiation.</td>
      <td>150</td>
    </tr>
    <tr>
      <td>5.30 The world oracle.</td>
      <td>151</td>
    </tr>
    <tr>
      <td>5.31 A sequence of rule applications showing an execution of the initial setting presented in the previous paragraphs.</td>
      <td>152</td>
    </tr>
  </tbody>
</table>
<table><tr><td>5.32 Two sequences of rule applications showing executions of the new setting that considers two clients. The first one is a trace showing an interaction producing an interesting physical event, and the second one does not show this interaction.</td><td>154</td></tr><tr><td>5.33 Two diagrams representing the evaluation functions. The diagram A depicts the non-deterministic evaluation function, and the diagram B depicts the scheduler's one.</td><td>157</td></tr><tr><td>5.34 Filtering functions on Π, where lfilter is the classic filter function on lists in functional programming.</td><td>161</td></tr><tr><td>5.35 Semantic rules for Step 1</td><td>162</td></tr><tr><td>5.36 Semantic rules for Step 2</td><td>163</td></tr><tr><td>5.37 Semantic rules for Step 3</td><td>164</td></tr><tr><td>5.38 Semantic rules for Step 4</td><td>165</td></tr><tr><td>5.39 Semantic rules for Step 5</td><td>166</td></tr><tr><td>5.40 Semantic rules for Step 6</td><td>167</td></tr><tr><td>5.41 Semantic rules for Step 7</td><td>168</td></tr><tr><td>5.42 At the top of the figure, we show an informal generic definition of the lemmas. The table shows, for each rule, the rules with which to commute and the constraints of the commutations.</td><td>170</td></tr><tr><td>5.43 Two scheduler's reordered traces behaviorally equivalent to the traces in Figure 5.32. With equivalent we mean that they produce the same final WEBI configuration. We annotate the some rules applications with "o" and "w" to refer to the oven and window service, and "a" and "s" to refer to the clients adam and steve.</td><td>179</td></tr></table>
A papá, mamma ed Amin,
un enorme piccola famiglia.
<figure><img src="image_9.png" /></figure>
# Introduction
the learning curve to access one of these methods.

Writing a formalization on paper works great on small calculi, as scientists can directly provide a formal meaning to the syntactical elements of a language by writing the behavior in a semantic style. Still, the complexity of writing full-scale programming languages on paper is challenging. These definitions become easily massive, non-manageable, or writable, and coherence can be challenging to maintain. Then informal proofs, the ones made by hand, can be pretty unreliable as the language formalization grows. Assuming that the work is safe and sound after tremendous efforts, it is difficult to derive an implementation from it, making it hard to test concretely. We would like to recall that this scientific area aims to find formalisms and technologies to reduce deficiencies in programming language specifications and implementations, goal that we cannot be sure to be hit by simply unit-test interpreters or compilers.

The machines' support has been an important breakthrough for semanticists. For example, via machine, one can automatically check the coherence of the formalization while writing it. In the last three decades, different tools and techniques machine-checked spread out. We can factorize them in two different macro-approaches: Semantics via *proof assistants*, such as Coq [70], HOL [29], Isabelle [30], or Twelf [71, 27], and Semantics via *specification languages*, such as Ott [66], Lem [55], K [63], or PLT [36].

The use of proof assistants allows to formally verify that programming languages uphold certain language-specific properties. In general, these frameworks are designed to reason about formal properties of mathematical objects. Excellent work has been done on the proof assistants; CompCert [18, 5, 4] for C, CakeML [12, 48, 69] for StandardML [68, 44], and JSCert project [7, 6] for JavaScript are some strong examples. Nevertheless, these technologies, despite their great power, work with their own logic, making the portability of a work, from a proof assistant to another almost impossible. The sources are cluttered with syntactic noise and generally, one needs to know at best the tool. Moreover, these are complex tools, making hard to be fluent in more than one tool, as the learning curve is steep. The result is a lack of exchange between different communities of proof assistants, as these technologies have created different schools of thought. This impacts collaboration between scientists, not being able to port these accomplishments into different platforms, even automatically. Indeed, these languages are complex, making mechanisms of executable code extraction hard to design and to be proven correct. For example, works such as the JSCert project put trust on the Coq
extraction method to OCaml [19], without having any formal guarantee of semantics mismatches.

This thesis is set in the context of semantics via specification languages. These languages, generally meta-languages, are built on theoretical frameworks, each with its peculiarities, to provide an intuitive way to implement the semantics of a programming language. Generally tiny languages, these works offer tools to generate artifacts to execute and formally study a formalization.

In the thesis, we will focus on the Skeletal Semantics framework. After providing a bit of background about semantic styles and how to use them to encode the behavior of a variant of a Vanilla While language in Chapter 1, in Chapter 2 we present the Skeletal Semantics and the tools for producing artifacts. These two chapters will offer a solid background to the thesis.

Then, in Chapter 3, we will present an approach for writing semantics in Skel, the language for writing Skeletal Semantics. This work is currently under major revision by the authors[35]. We claim our techniques produce concise, readable, and maintainable semantics. This novel approach to specification languages allows exploiting continuations in our meta-language to design carefully chosen monad and hide side-effects in the programming language formalizations. Formalizations are structurally solid, and extending them means encoding the evaluation behavior of the language constructs and updating the monads. The core of the language stays immutated.

Chapter 4 presents the work published in the proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming and of the 32nd Journées Francophones des Langages Applicatifs [34, 33]. We apply the technique presented in Chapter 3 by providing a formal semantics of ECMAScript and showing how to use our monadic approach to build a solid and extensible formalization of the JavaScript specification.

Finally, in Chapter 5, we present a model that aims to embody the behavior of a distributed system for IoT applications. This orchestrating semantics, tiny in size, models complex interactions between tiers, and writing it in Skel is still a challenge. Nevertheless, we propose the semantics and a naïve implementation. Then, to constrain the model's non-determinism, we produce a scheduling policy easily implementable in Skel, proven correct and complete.
# PART I

## Background
<figure><img src="image_10.png" /></figure>
# SEMANTIC STYLES

## Contents

<table><tr><td>1.1</td><td>A While Language</td><td>8</td></tr><tr><td>1.2</td><td>Operational Semantics</td><td>10</td></tr><tr><td>1.2.1</td><td>Structural Operational Semantics</td><td>11</td></tr><tr><td>1.2.2</td><td>Big-Step Operational Semantics</td><td>15</td></tr><tr><td>1.3</td><td>Abstract Machines</td><td>18</td></tr><tr><td>1.4</td><td>Pretty-Big-Step Semantics</td><td>21</td></tr></table>

« A thing named, misnamed, unnamed, or renamed is still itself. »

- Mokokoma Mokhonoana

## Introduction

We define a programming language by its syntax, which is related to the grammatical structure of programs, and semantics, which is more concerned with expressing the meaning of a program. As the thesis presents an efficient and concise approach for capturing semantics, this chapter provides some background on general techniques that have historically and recently been used for defining the behavior of programming language constructs. Generally speaking, the goal of a formal semantics is to define rigorously/mathematically the meaning of the programs written in the considered programming language. The task is quite challenging, especially considering complex programming languages. Nevertheless, the implications are interesting, as formalizations can be declined in multiple applications of interest. For example, a formalization helps reveal ambiguities or inconsistencies in a programming language specification. It can also be a valid support for writing ground-truth implementations of interpreters.
## Syntax of the While Language

NUM $n \in \mathbb{Z}$, extensionally $\{\dots, -1, 0, 1, \dots\}$

BOOL $b \in \{T, F\}$, respectively true and false

VALUE $v ::= n | b$

VAR $x \in \Sigma^+$, where $\Sigma$ is an alphabet of our choice. i.e. $\{a, b, \dots, z\}$

STORE $\sigma : VAR \rightarrow VALUE$

EXPR $e ::= v | x | e_1 \diamond e_2 | e_1 \circ e_2 | e_1 \odot e_2 | !e$

CMD $c ::= \mathbf{skip} | x := e | c_1; c_2 | \mathbf{if}(e)\{c_1\} \mathbf{else} \{c_2\}$

while(e){c}

<caption>Figure 1.1: Definition of the While language grammar.</caption>

Moreover, often tools are built around these representations to perform, for example, analysis of programs and formal verification.

In this chapter, we introduce different ways of describing formally programming languages semantics and the notation used throughout all thesis. In detail, Section 1.1 presents a simple While language. Then, we present first the two operational semantics (Section 1.2), in Sections 1.2.1, 1.2.2, respectively, the Plotkin's *Structural Operational Semantics* (SOS), the *Natural Semantics* (NS), moving then to the *Abstract Machines* (AM) in Section 1.3, and the non-classical *Pretty-Big-Step Semantics* (PBS) in Section 1.4. For each of the semantic styles, we embed the While language variant presenting semantic rules for the expressions and statements, highlighting the limitations of each formal framework. This chapter aims to show textbook approaches to semantics as we base the design of the languages we present in the thesis on these semantic styles.

# 1.1 A While Language

The While language is a simple imperative language. In Figure 1.1 we define its syntax via a simplified Backus-Naur form [3] (BNF).

A VALUE can be either an integer or a booleans. We define the store as a partial map from variables to values. If a variable $x$ is not bound in $\sigma$, the operation $\sigma(x)$ fails.
Otherwise, it returns the bound value. Given a variable $x$, we define $\sigma + x \rightarrow v$ as the environment extension or update, binding $x$ to a value $v$.

Expressions can be values, variables, binary arithmetic operations (denoted as $\diamond$), logical binary operations (denoted as $\circ$), or the $!$ operator. We define $\diamond \in \{+, -, *, /\}$ and $\circ \in \{\ge, >, \le, <, =, \wedge, \vee\}$. We call the concrete logical binary operations on integers and booleans, respectively $\circ_Z$ and $\circ_B$, to denote comparisons between integers or between booleans. Similarly, we define $\diamond_Z$ and $\circ_B$ as the concrete operations for computing arithmetic and unary expressions, respectively, between integers and on booleans. Notice that we partially define these operators, as we only allow evaluations producing values of the type denoted by the subscript. By design, a legal program can be an expression that reduces to, for example, $T+4$. We can freely decide on a strategy to evaluate the binary expressions. An approach can be one that does not allow such a thing to happen. We can define a partial function that only produces a result when the two subexpressions reduce to the same type. $T+4$ fails in this case, as we chose to define operators partially. Otherwise, one can enrich the language, making the evaluation return either the expected result or an exception. This approach can be interesting for capturing non-allowed behaviors, such as division by 0. Finally, one can allow these mixed expressions to happen. This approach is more related to *dynamically typed languages*. A naïve strategy can be to evaluate the two subexpressions and give the result according to the type of the first value argument. This evaluation strategy must treat *unsafe coercions*—implicit operations that change the values' type-.

For simplicity, we present a partial semantics, meaning that if no rule reduces a language constructor, the evaluation becomes stuck.

Once we reduce the two subexpressions for arithmetic operators, we can check both values to ensure type concordance. The result of an arithmetic expression is a numeric value. The result of an arithmetic expression is a numeric value.

We define the evaluation only with type concordance for the comparative logical expressions, concretely represented by $\circ_Z$ and $\circ_B$, while for the pure logical expressions, we allow only boolean values to be elements of the expression, concretely $\circ_B$. We permit boolean comparison by saying that the relation $(T > F) = T$, and $(T \neq F) = T$. For what concerns the $!$ operator, if we negate a boolean, the function returns its complement. We proceed with the partial approach, allowing only the negation of a boolean.

To gently introduce evaluation descriptions, in Figure 1.2, we present a simple partial function $\phi$ that evaluates the expressions of the `While` language. Further encodings
$$ \phi : \mathbf{Expr} \times \mathbf{Store} \rightarrow \mathbf{Value} $$

$$ \phi(e, \sigma) = \begin{cases} \sigma(x), & \text{if } e = x, \text{ a variable} \\ v, & \text{if } e = v, \text{ a value.} \\ n_1 \diamond \mathbb{Z} \, n_2, & \text{if } e = (e_1 \diamond e_2) \text{ and } \phi(e_1, \sigma) = n_1 \text{ and } \phi(e_2, \sigma) = n_2. \\ n_1 \circ \mathbb{Z} \, n_2, & \text{if } e = (e_1 \circ e_2) \text{ and } \phi(e_1, \sigma) = n_1 \text{ and } \phi(e_2, \sigma) = n_2. \\ b_1 \circ \mathbb{B} \, b_2, & \text{if } e = (e_1 \circ e_2) \text{ and } \phi(e_1, \sigma) = b_1 \text{ and } \phi(e_2, \sigma) = b_2. \\ b_1 \odot \mathbb{B} \, b_2, & \text{if } e = (e_1 \odot e_2) \text{ and } \phi(e_1, \sigma) = b_1 \text{ and } \phi(e_2, \sigma) = b_2. \\ !b, & \text{if } e = !e' \text{ and } \phi(e', \sigma) = b. \end{cases} $$

<caption>Figure 1.2: Expression evaluation function $\phi$</caption>

```pascal
n := 3;b := 3;r := 1;
while(n > 0){
  r := r * b;
  n := n - 1
}
```

<caption>Figure 1.3: Example</caption>

of the expression's behavior will match the one described by this function.

The CMD syntactic production describes the commands of the language. These can be a skip, a variable assignment, a command sequencing, a conditional if-else, or a loop statement while.

In the listing in Figure 1.3, we show an example of a program. It computes in r the n-th power of a number b, $3^3$ in the example.

## 1.2 Operational Semantics

An Operational Semantics of a programming language describes how programs execute. The approach consists in formally defining the meaning of each of the syntactic constructs of the language via logical relations. The abstraction helps avoid details related to the description of the machine that is supposed to execute a program. Indeed, concepts like the memory model, the machine architecture, and the implementation
tation details of an interpreter are irrelevant, as the goal is to describe how to derive meaning from a language construct rather than a concrete implementation. To resume, operational semantics only describes what happens if a construct of the language is evaluated.

In general, for the operational semantics, a transition relation produces a judgment from one program configuration to another by applying an inference rule.

An inference rule has a set of premises on top of the line and the conclusion below the line. The conclusion is valid if all the premises are satisfied. Then, an inference rule without premises is called axiom, which is always true. We show them below.

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

A judgment is the result of a derivation built as a derivation tree. This structure represents the evaluation of an expression of the language. The root of this tree is the original expression, and each premise is a subtree of the derivation tree, justifying the evaluation of the expression. The conclusion is the resulting semantic judgement (evaluation) when the premises are satisfied. A conclusion is placed as the root of the derivation tree.

In the following two sections, we will present the *Structural Operational Semantics* and the *Natural Semantics* operationally, meaning that we will introduce them by formalizing the *While* language.

## 1.2.1 Structural Operational Semantics

The Structural Operational semantics goal is to describe computations in terms of their individual steps. Indeed, SOS is also known as Small-Step semantics. In 1981, Plotkin wrote the famous “Aarhus” notes [61], which first presented the *Structural approach for defining the “operational”– the meaning of the program - semantics via logical statements rather than partial functions, as done by using the denotational semantics* [73, 43]. The intention behind proposing this formal approach was to provide logical-relational meaning to the constructs of a programming language rather than a functional one. Indeed, the operational behavior of a programming language then is considered to be an abstraction, rather than a description, that could be used for proof
$$ \text{Store} \times \text{Expr} \downarrow_e \text{Store} \times \text{Expr} - \text{Store} \times \text{Expr} \downarrow_e \text{Value} $$

<figure><img src="image_12.png" /><figcaption>Figure 1.4: Small-Step expression evaluation. This description matches the behavior defined in Figure 1.2.</figcaption></figure>

of correctness, safety, or security.

Usually, a language construct's semantics can be defined in terms of the behavior of its parts, driving the evaluation by its syntactic structure. Then, the SOS program's evaluation can be seen as a sequence of transition relations that reduce the program to its final result. Indeed, each syntactic construct of a language has a set of inference rules that define its behavior–set of valid judgments– and each valid judgment, in this example, modifies and reduces the shape of the program. The program finishes evaluating when it is not possible to perform another transition. Thus, small-step semantics are ideal for watching the program execute step by step.

We define two different transition relations, one for evaluating expressions and the other for commands.

In the case of expressions, $\downarrow_e$ is a semantic judgment expressed as a relation between expression configurations $(\sigma, e) \downarrow_e (\sigma, e')$, or a relation between an expression configuration and a value $(\sigma, e) \downarrow_e v$. A configuration is a pair (STORE, EXPR). In Figure 1.4, we present a small-step operational semantics for evaluating expressions, according to the equational definition depicted in Figure 1.2.
$$ \text{Store} \times \text{CMD} \downarrow_c \text{Store} \times \text{CMD} - \text{Store} \times \text{Expr} \downarrow_c \text{Store} $$

<figure><img src="image_13.png" /><figcaption>Figure 1.5: Small-Step commands evaluation.</figcaption></figure>

Regarding commands, we define the relation $\downarrow_c$ to be either a relation between command configurations $(\sigma, c) \downarrow_c (\sigma', c')$ or a relation $(\sigma, c) \downarrow_c \sigma'$. Similarly, a configuration is a couple (STORE, CMD). Regarding the store, we define two operations. The first is for getting a binding from the store: given a store $\sigma$ and a variable $x$, $\sigma(x)$ returns a value. The second operation is the store extension/update: given a store $\sigma$, variable $x$, and a value $v$, $\sigma + (x \rightarrow v)$ returns the store $\sigma$ updated with the binding $x \rightarrow v$. We present the definition of the While language behavior in Figure 1.5.

If we consider the `if-else` construct rules, we notice that for evaluating it, first, we have to evaluate the guard condition. As we know, it might take several steps. Once the condition is evaluated to a value, the rules `IFT` and `IFF` put the first or second branch into evaluation. No reductions are yet done on $c_1$ or $c_2$. For the `while` command evaluation, we notice that the `WHILE` rule changes only the program's structure to an `if-else`. This judgment changes the structure of the initial syntactic construct without performing any reduction of the statement itself. It is one of the reasons that this semantics is called structural, as it reasons on the structure of the program, sometimes by reducing
it, and sometimes by transforming it to something equivalent.

In the following listing, we show concretely the use of a small-step semantics to reduce a program. We consider the program presented in Figure 1.3, initially having an empty store $\sigma$, denoted as $\emptyset$.

( $\emptyset, n := 3; b := 2; r := 1; \text{while}(b > 0) \{ r := r * n; b := b - 1 \}$ )

Then, the following shows the program reductions.

↓<sub>c</sub> ([n→3], b := 2; r := 1; while(b > 0) { r := r * n; b := b - 1 })

↓<sub>c</sub> ([n→3,b→2], r := 1; while(b > 0) { r := r * n; b := b - 1 })

↓<sub>c</sub> ([n→3,b→2,r→1], while(b > 0) { r := r * n; b := b - 1 })

↓<sub>c</sub> ([n→3,b→2,r→1], if(b > 0) { r := r * n; b := b - 1; while(b > 0) {...}} else {skip})

↓<sub>c</sub> ([n→3,b→2,r→1], if(2 > 0) { r := r * n; b := b - 1; while(b > 0) {...}} else {skip})

↓<sub>c</sub> ([n→3,b→2,r→1], if(T) { r := r * n; b := b - 1; while(b > 0) {...}} else {skip})

↓<sub>c</sub> ([n→3,b→2,r→1], r := r * n; b := b - 1; while(b > 0) { r := r * n; b := b - 1 })

↓<sub>c</sub> ([n→3,b→2,r→1], r := 1 * n; b := b - 1; while(b > 0) { r := r * n; b := b - 1 })

↓<sub>c</sub> ([n→3,b→2,r→1], r := 1 * 3; b := b - 1; while(b > 0) { r := r * n; b := b - 1 })

↓<sub>c</sub> ([n→3,b→2,r→1], r := 3; b := b - 1; while(b > 0) { r := r * n; b := b - 1 })

↓<sub>c</sub> ([n→3,b→2,r→3], b := b - 1; while(b > 0) { r := r * n; b := b - 1 })

↓<sub>c</sub> ([n→3,b→2,r→3], b := 2 - 1; while(b > 0) { r := r * n; b := b - 1 })

↓<sub>c</sub> ([n→3,b→2,r→3], b := 1; while(b > 0) { r := r * n; b := b - 1 })

↓<sub>c</sub> ([n→3,b→1,r→3], while(b > 0) { r := r * n; b := b - 1 })

↓<sub>c</sub> ([n→3,b→1,r→3], if(b > 0) { r := r * n; b := b - 1; while(b > 0) {...}} else {skip})

↓<sub>c</sub> ([n→3,b→1,r→3], if(1 > 0) { r := r * n; b := b - 1; while(b > 0) {...}} else {skip})

↓<sub>c</sub> ([n→3,b→1,r→3], if(T) { r := r * n; b := b - 1; while(b > 0) {...}} else {skip})

↓<sub>c</sub> ([n→3,b→1,r→3], r := r * n; b := b - 1; while(b > 0) { r := r * n; b := b - 1 })

↓<sub>c</sub> ([n→3,b→1,r→3], r := 3 * n; b := b - 1; while(b > 0) { r := r * n; b := b - 1 })

↓<sub>c</sub> ([n→3,b→1,r→3], r := 3 * 3; b := b - 1; while(b > 0) { r := r * n; b := b - 1 })

↓<sub>c</sub> ([n→3,b→1,r→3], r := 9; b := b - 1; while(b > 0) { r := r * n; b := b - 1 })

↓<sub>c</sub> ([n→3,b→1,r→9], b := b - 1; while(b > 0) { r := r * n; b := b - 1 })

↓<sub>c</sub> ([n→3,b→1,r→9], b := 1 - 1; while(b > 0) { r := r * n; b := b - 1 })

↓<sub>c</sub> ([n→3,b→1,r→9], b := 0; while(b > 0) { r := r * n; b := b - 1 })

↓<sub>c</sub> ([n→3,b→0,r→9], while(b > 0) { r := r * n; b := b - 1 })

↓<sub>c</sub> ([n→3,b→0,r→9], if(b > 0) { r := r * n; b := b - 1; while(b > 0) {...}} else {skip})

↓<sub>c</sub> ([n→3,b→0,r→9], if(0 > 0) { r := r * n; b := b - 1; while(b > 0) {...}} else {skip})

↓<sub>c</sub> ([n→3,b→0,r→9], if(F) { r := r * n; b := b - 1; while(b > 0) {...}} else {skip})
$\downarrow_c ([n \to 3, b \to 0, r \to 9], \text{skip})$

$\downarrow_c [n \to 3, b \to 0, r \to 9]$

We can see that this program computes $r = n^b$. For the initial assignments of $n = 3$, $b = 2$, and $r = 1$, we get $r = 9$, as expected.

Notice that each small step performed on the program configuration is a derivation tree for SOS. The sequence of transitions is a sequence of derivation trees, and each derivation tree is a small-step judgment. Indeed, the number of derivation trees equals the number of transition relations applied. Then, each tree has as many subtrees as the premises of the rule applied by that transition relation. Intuitively, an infinite sequence of derivation steps on a program represents a diverging computation.

### 1.2.2 Big-Step Operational Semantics

Different from small-step semantics, big-step, originally called *natural semantics* [32], is more concerned with the relationship between an execution's initial and final configuration. Indeed, here the description of the semantics focuses on describing the overall execution of a program rather than tracing each step. Then a big-step judgment can successfully give a result, gets stuck as no rule applies, or never terminate. Notice that, as the natural semantics focuses more on representing the overall judgment in one single big step, there is no way to understand if a derivation is stuck or does not terminate. Usually, languages represented in big-step semantics result in a more concise rule-set.

For what concerns expressions, differently from what we have presented in Section 1.2.1, we now evaluate expressions in one step. So, first, we re-define the transition relation $\downarrow_e$, as $\Downarrow_e$. The new relation, relates expression configurations (STORE, EXPR) to values. The VARIABLE rule does not change much, and we present it below.

VARIABLES

$$ \frac{\sigma(x) = v}{\sigma, x \Downarrow_e v} $$

Let us consider comparison expressions, which are the expressions with more related rules. We can see that the number of rules reduces dramatically by bunching
Store × CMD ⇓c Store

<figure><img src="image_14.png" /><figcaption>Figure 1.6: Commands Evaluation in Big-Step</figcaption></figure>

the premises of the rules together.

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

Considering the new relation ⇓e, we can immediately notice that a rule now is written in terms of evaluating its subterms, describing the overall result of the evaluation as a final judgment. In Figure 1.6, we present the big-step definition of the While language. The evaluation relation ⇓c is between a configuration (σ, c) and a store σ.

Then, evaluating the program depicted in Figure 1.3 results simply in the following.
(Ø, n := 3; b := 2; r := 1; while (e > 0) { r := r * n; b := b - 1 })

غو دو دو دو
c
[ n → 3 , b → 0 , r → 9 ]

Notice that, differently from the small-step semantics, in this case, the overall derivation
is no more a sequence of relation applications. However, it is a unique derivation tree
containing all the other judgements, the ones of its subtrees. We present a partial
<figure><img src="image_16.png" /><figcaption>Figure 1.7: First level of the big-step derivation tree of the program. We put ... when we refer to the rest of the program.</figcaption></figure>
derivation tree in Figure 1.7.

Moreover, looking back at the rules, different from the SOS, natural semantics
seems more structured on where to place the premises in a rule. Indeed, one can
see premises more like a sequence rather than a set.

The big-step semantics does not perform any syntactic transformation of terms. An
example is the `while` command, which, differently from the SOS—term transformation
into an `if-`, is "naturally" evaluated.

1.3 Abstract Machines

The correctness of programming language implementations is an important issue con-
fronting language designers and implementors. Traditionally, such implementations are
handcrafted first and only then proved correct. Unfortunately, keeping a strong relation-
ship between a formal specification and its implementation may be challenging to show.
Indeed, one must relate several details to its formal representation. Alternatively, a lan-
guage implementation can be constructed from the semantic specification so that the
resulting implementation guarantees correctness.

Abstract machines (AM) [38] can provide an intermediate representation of the lan-
guage's implementation that remains loyal to its operational semantics [26]. As we have
seen in Section 1.2, operational semantics can be defined in terms of inference rules.
An equivalent abstract machine can be built as rewriting rules describing single-step
operations on the state of a computation. Such specifications provide an intermediate
level of representation for many practical implementations of programming languages.
Abstract machines are traditionally constructed by hand, with correctness proofs that
follow independently.

For building an AM for the *While* language, we first define three states/modes for the
machine. The first two states set the machine to evaluate expressions or statements.
We denote the two respectively as 〈*c*, *π*, *σ*〉<sub>CMD</sub> or 〈*e*, *π*, *σ*〉<sub>EXPR</sub>, meaning that a command
or an expression is evaluated in a state *σ* with a continuation stacked in *π*. The third
mode signals the result to another computation frame waiting for a result. In the normal
case, it communicates the value to the top pending computation frame, which is the
top of the stack *π*. We denote two continuation modes. The first continuation mode
[π, *σ*, *r*]c propagates a value to the top-continuation stacked in *π* in a state *σ*. The second
continuation mode [π, *σ*]c returns the state—it is similar to return a unit result.
Expression Evaluation AM

$$ \langle v, \pi, \sigma \rangle_{\text{EXPR}} \rightarrow [\pi, \sigma, v]_c \qquad (1.1) $$

$$ \langle x, \pi, \sigma \rangle_{\text{EXPR}} \rightarrow [\pi, \sigma, \sigma(x)]_c \qquad (1.2) $$

$$ \langle e_1 \diamond_C e_2, \pi, \sigma \rangle_{\text{EXPR}} \rightarrow \langle e_1, (\square \diamond_C e_2) :: \pi, \sigma \rangle_{\text{EXPR}} \qquad (1.3) $$

$$ [(\square \diamond_C e_2) :: \pi, \sigma, v_1]_c \rightarrow \langle e_2, (v_1 \diamond_C \square) :: \pi, \sigma \rangle_{\text{EXPR}} \qquad (1.4) $$

$$ [(b_1 \diamond_C \square) :: \pi, \sigma, b_2]_c \rightarrow [\pi, \sigma, b_1 \diamond_C b_2]_c \qquad (1.5) $$

$$ [(n_1 \diamond_C \square) :: \pi, \sigma, n_2]_c \rightarrow [\pi, \sigma, n_1 \diamond_C n_2]_c \qquad (1.6) $$

<caption>Figure 1.8: Abstract Machine definition of expression evaluation.</caption>

An AM stops evaluating once there are no more things to do. Nothing to do means that $\pi$ becomes empty. If no rule is applicable, then the machine gets stops.

For instance, an AM is defined by its rewriting relation $\rightarrow$, relating computations.

As we did for the expressions, in Section 1.2.2, Figure 1.8 presents the AM transition rules for variables, the comparative logical expressions, adding the rule that signals convergence to a value. For instance, if we consider the evaluation of a value $v$, rule 1.1, the transition switches the expression evaluation mode to the continuation one, signaling to the top of $\pi$, the value $v$. Similarly, evaluating a variable $x$, rule 1.2, means to switch to a continuation mode carrying, as a result, the value bound to $x$ in $\sigma$, $\sigma(x)$. Then, for evaluating a comparative logical expression, when computing the first argument of $e_1 \diamond e_2$ (rule 1.3), we set $e_1$ to be evaluated and push $\square \diamond e_2$ onto the stack as the top pending evaluation. The expression with the hole is a frame stating that we are evaluating a comparative logical expression, and $e_1$ is set to evaluation. Once the evaluation of $e_1$ is complete, applying the frame $\square \diamond e_2$ to the value $v_1$ means switching back to evaluation mode for $e_2$ with a new stacked frame $v_1 \diamond \square$ (rule 1.4) on top of $\pi$. Notice that the frame $\square \diamond e_2$ is popped, and the top of the stack now stores the value $v_1$. Finally, applying $v_1 \diamond \square$ to a value $v_2$ computes $v_1 \diamond v_2$, depending on the type concordance of the values $v_1$ and $v_2$ (rules 1.5 to 1.6), as defined in Figure 1.2. If the types of the values mismatch, the abstract machine gets stuck.

At this point, we can note a similarity to the small-step semantics, as the abstract machine evolves step by step. For example, rule 1.3, sets $e_1$ to evaluation. Then depending on the expression's complexity, we need to apply several different rules to converge to a result.
Commands Evalaution AM

$\langle \mathbf{skip}, \pi, \sigma \rangle_{\text{CMD}} \rightarrow [\pi, \sigma]_c$
$\langle x := e, \pi, \sigma \rangle_{\text{CMD}} \rightarrow \langle e, (x := \Box) :: \pi, \sigma \rangle_{\text{EXPR}}$
$[(x := \Box) :: \pi, \sigma, v]_c \rightarrow \langle \mathbf{skip}, \pi, (\sigma + x \rightarrow v) \rangle_{\text{CMD}}$
$\langle c_1; c_2, \pi, \sigma \rangle_{\text{CMD}} \rightarrow \langle c_1, c_2 :: \pi, \sigma \rangle_{\text{CMD}}$
$\langle \mathbf{if}(e)\{c_1\}\mathbf{else}\{c_2\}, \pi, \sigma \rangle_{\text{CMD}} \rightarrow \langle e, (\mathbf{if}(\Box)\{c_1\}\mathbf{else}\{c_2\}) :: \pi, \sigma \rangle_{\text{EXPR}}$
$[(\mathbf{if}(\Box)\{c_1\}\mathbf{else}\{c_2\}) :: \pi, \sigma, T]_c \rightarrow \langle c_1, \pi, \sigma \rangle_{\text{CMD}}$
$[(\mathbf{if}(\Box)\{c_1\}\mathbf{else}\{c_2\}) :: \pi, \sigma, F]_c \rightarrow \langle c_2, \pi, \sigma \rangle_{\text{CMD}}$
$\langle \mathbf{while}(e)\{c\}, \pi, \sigma \rangle_{\text{CMD}} \rightarrow \langle \mathbf{if}(e)\{c; \mathbf{while}(e)\{c\}\} \mathbf{else}\{\mathbf{skip}\}, \pi, \sigma \rangle_{\text{CMD}}$

<caption>Figure 1.9: Abstract Machine definition of commands evalauation.</caption>

If we consider an initial machine $\langle 1 < 2, \epsilon, [] \rangle_{\text{EXPR}}$, where $\epsilon$ is the empty stack, then
we can derive the following sequence.

$\langle 1 < 2, \epsilon, [] \rangle_{\text{EXPR}} \rightarrow$
$\langle 1, (\Box < 2) :: \epsilon, \sigma \rangle_{\text{EXPR}} \rightarrow$
$[(\Box < 2) :: \epsilon, \sigma, 1]_c \rightarrow$
$\langle 2, (1 < \Box) :: \epsilon, \sigma \rangle_{\text{EXPR}} \rightarrow$
$[(1 < \Box) :: \epsilon, \sigma, 2]_c \rightarrow$
$[\epsilon, \sigma, 1 < 2]_c = [\epsilon, \sigma, T]_c$

The expression results in T, as expected. Note that each subexpression is first set to
evaluation, then concretely evaluated.

$\langle \mathbf{add}(1, 1), \epsilon \rangle_{\text{EXPR}} \rightarrow \langle 1, \mathbf{add}(\Box, 1) :: \epsilon \rangle_{\text{EXPR}} \rightarrow$
$[\mathbf{add}(\Box, 1) :: \epsilon, 1]_c \rightarrow \langle 1, \mathbf{add}(1, \Box) :: \epsilon \rangle_{\text{EXPR}} \rightarrow$
$[\mathbf{add}(1, \Box) :: \epsilon, 1]_c \rightarrow [\epsilon, 1]_c$

Similarly, we can formalize commands semantics via AM. We present the abstract
machine representing the semantics of the language in Figure 1.9.
## 1.4 Pretty-Big-Step Semantics

Our *While* language is dynamically typed, in the sense that there is no check that undefined operations such as $T + 4$ are absent, hence a program can become stuck. Moreover, we know that a big step evaluation of a program can be either infinite, in the case there is always a rule able to apply, stuck when there is none, or stop when it reaches a result. The problem for the Natural Semantics (NS) is that it is hard to know whether the evaluation is converging to a result or is stuck because something wrong happened—its original goal was to express the semantics of terminating programs. For example, following our previous language definitions, we have never considered handling the division by zero by allowing a failure in the evaluation.

If we consider the division by zero in NS, then we need to tweak the syntax and the semantics to carry the information about a failure to the top level and not simply get blocked somewhere in the middle of the program evaluation. For example, we can define an *option type* and say that a semantic judgment of an expression($\Downarrow_e$) either exists, denoted as $\mathit{Some} v$, where $v$ is the result of evaluating an expression, or $\mathit{None}$ when a failure, for instance, division by zero, happens. Now, consider the addition and the division rule considering the new big-step relation for expressions presented in Figure 1.10. We notice that, by only expressing the failure to the parent node in the derivation tree, we increase the number by a factor of at least three: from three to nine. The description of the addition consists of three rules: the first two, ADDF1 and ADDF2, state the failure of the evaluation of $e_1$ or $e_2$, and the third evaluates the addition (ADD). For the division rules, things are pretty similar, having one rule more preventing division by zero. Notice the redundancy in the premises. The rules ADDF1 and ADDF2 are basically the same as DIVF1, and DIVF2.

Moreover, the ADD, and the two DIV and DIV0 share most of the rule premises. To be precise, the number of $\Downarrow_e$ in the premises of the addition are 5, and 7 for the division. These redundancies can be really annoying while trying to prove by structural induction properties of the language. Indeed it leads to consider several times the same transition relation, proving more than once the same proof sub-tree. To sum up, the handling of the exceptions is explicit and redundant, making formalizations and proofs grow both in size and complexity even for one more piece of information carried around through derivations. So, can we factorize the big-step rules to avoid redundancies?

The answer is yes; we can do it by changing the formal definition of the program-
Store × Expr ⇓e Opt

ADDF1
$\sigma, e_1 \Downarrow_e \text{None}$
$\frac{}{\sigma, e_1 + e_2 \Downarrow_e \text{None}}$

ADDF2
$\sigma, e_1 \Downarrow_e \text{Some } n_1$
$\frac{}{\sigma, e_2 \Downarrow_e \text{None}}$
$\frac{}{\sigma, e_1 + e_2 \Downarrow_e \text{None}}$

ADD
$\sigma, e_1 \Downarrow_e \text{Some } n_1$
$\sigma, e_2 \Downarrow_e \text{Some } n_2$
$\frac{n = n_1 + n_2}{\sigma, e_1 + e_2 \Downarrow_e \text{Some } n}$

DIVF1
$\sigma, e_1 \Downarrow_e \text{None}$
$\frac{}{\sigma, e_1/e_2 \Downarrow_e \text{None}}$

DIVF2
$\sigma, e_1 \Downarrow_e \text{Some } n_1$
$\frac{}{\sigma, e_2 \Downarrow_e \text{None}}$
$\frac{}{\sigma, e_1/e_2 \Downarrow_e \text{None}}$

DIV0
$\sigma, e_1 \Downarrow_e \text{Some } n_1$
$\frac{}{\sigma, e_2 \Downarrow_e \text{Some } 0}$
$\frac{}{\sigma, e_1/e_2 \Downarrow_e \text{None}}$

DIV
$\sigma, e_1 \Downarrow_e \text{Some } n_1$
$\sigma, e_2 \Downarrow_e \text{Some } n_2$
$\frac{n_2 \neq 0}{\sigma, e_1/e_2 \Downarrow_e \text{Some } n}$
$\frac{n = n_1/n_2}{\sigma, e_1/e_2 \Downarrow_e \text{Some } n}$

<caption>Figure 1.10: Expression Evaluation with Option Results in Big-Step</caption>

ming language. Arthur Charguéraud introduced the pretty-big-step semantics [15] to factorize the description of both effectful programming languages and managing to capture divergent programs while analyzing programs. This semantics preserves the big-step philosophy by keeping the overall reduction of a program happening in a single transition relation application. However, the big-step and the pretty-big-step derivation trees are quite different, as the PBS rules decouple syntactic constructs and effects behaviors. Let us try to write the addition and division rules, considering division by zero. The idea is to decouple the behavior of a syntactic construct from the actual effect that the evaluation of a subterm carries. We re-define only addition and division, but the approach must be extended to the rest of the arithmetic and logical expressions.

Expression Syntax in Pretty-Big-Step

OPT $o$ ::= None | Some $v$

EXPR $e$ ::= $o$ | $x$ | $e_1 + e_2$ | $o_1 +_1 e_2$ | $v_1 +_2 o_2$ | $e_1/e_2$ | $o_1 /_1 e_2$ | $v_1 /_2 o_2$
Store × Expr ⇒$_{e}$ Opt

ADD

$$
\frac{
  \begin{array}{l}
    \sigma, e_1 \Rightarrow e o_1 \\
    \sigma, o_1 +_1 e_2 \Rightarrow e o \\
    \hline
    \sigma, e_1 + e_2 \Rightarrow e o
  \end{array}
}{
  \sigma, e_1 + e_2 \Rightarrow e o
}
$$

ADDF1

$$
\sigma, \text{None} +_1 e_2 \Rightarrow_e \text{None}
$$

ADD1

$$
\frac{
  \begin{array}{l}
    \sigma, e_2 \Rightarrow_e o_2 \\
    \sigma, n_1 +_2 o_2 \Rightarrow_e o \\
    \hline
    \sigma, (\text{Some } n_1) +_1 e_2 \Rightarrow_e o
  \end{array}
}{
  \sigma, (\text{Some } n_1) +_1 e_2 \Rightarrow_e o
}
$$

ADDF2

$$
\frac{\sigma, n_1 +_2 \text{None} \Rightarrow_e \text{None}}{\sigma, n_1 +_2 \text{None} \Rightarrow_e \text{None}}
$$

ADD2

$$
\frac{n = n_1 + n_2}{\sigma, n_1 +_2 (\text{Some } n_2) \Rightarrow_e \text{Some } n}
$$

DIV

$$
\frac{
  \begin{array}{l}
    \sigma, e_1 \Rightarrow_e o_1 \\
    \sigma, o_1 /_1 e_2 \Rightarrow_e o \\
    \hline
    \sigma, e_1 / e_2 \Rightarrow_e o
  \end{array}
}{
  \sigma, e_1 / e_2 \Rightarrow_e o
}
$$

DIVF1

$$
\frac{\sigma, \text{None} /_1 e_2 \Rightarrow_e \text{None}}{\sigma, \text{None} /_1 e_2 \Rightarrow_e \text{None}}
$$

DIV1

$$
\frac{
  \begin{array}{l}
    \sigma, e_2 \Rightarrow_e o_2 \\
    \sigma, n_1 /_2 o_2 \Rightarrow_e o \\
    \hline
    \sigma, (\text{Some } n_1) /_1 e_2 \Rightarrow_e o
  \end{array}
}{
  \sigma, (\text{Some } n_1) /_1 e_2 \Rightarrow_e o
}
$$

DIVF2

$$
\frac{\sigma, n_1 /_2 \text{None} \Rightarrow_e \text{None}}{\sigma, n_1 /_2 \text{None} \Rightarrow_e \text{None}}
$$

DIV0

$$
\frac{\sigma, n_1 /_2 (\text{Some } 0) \Rightarrow_e \text{None}}{\sigma, n_1 /_2 (\text{Some } 0) \Rightarrow_e \text{None}}
$$

DIV2

$$
\frac{n_2 \neq 0 \quad n = n_1/n_2}{\sigma, n_1 /_2 (\text{Some } n_2) \Rightarrow_e \text{Some } n}
$$

<caption>Figure 1.11: Expression Evaluation in Pretty-Big-Step</caption>

The presented syntax is a reformulation of the previous. This reformulation is a de-
composition that aims to split a few complex and redundant rules into a more significant
number of atomic rules. We show it in Figure 1.11. The pretty-big-step transition relation
for expressions is ⇒<sub>e</sub>, and it relates expression configurations (σ, e) to option values o.
To begin, we can say that now, for both the set of rules for addition and division, we
have only 4 ⇒<sub>e</sub> transitions in the premises. All these premises produce different proof
sub-trees. Thus, this formalization of the expressions is no more redundant.

Consider the PBS' addition rules. The ADD rule first evaluates expression $e_1$, which
results in an option value $o_1$, and then evaluates $o_1 +_1 e_2$. We can say that the rule
formulation does not state any failure of the evaluation, while it simply delegates the
check to another rule. Moreover, notice that the overall evaluation happens in a single
derivation tree that grows in depth. Then, for evaluating $o_1 +_1 e_2$, one can apply the
rule ADDF1 or ADD1 depending on whether the first expression failed or not. Notice
that the syntactic operators $+_1$ and $+_2$ define intermediate evaluation stages of the
## Expression Syntax in Pretty-Big-Step

```
RES r ::= Exc σ | σ
CMD c ::= skip | x := e | x :=_1 o | c₁; c₂ | r;_1 c₂ | if(e){c₁} else {c₂}
        | if1(o){c₁} else {c₂} | while(e){c}
```

<caption>Figure 1.12: Syntax definition of the language in Pretty-Big-Step style.</caption>

addition, respectively stating if either the first or the second expression evaluates to an option value. The rules `ADDF1` and `ADDF2` propagate a `None` result in case the first or the second addend fails while evaluating. If the first argument evaluates to `Some` value `n₁`, the rule `ADD1` evaluates the second expression to `o₂`, and then the result of the rule is the addition result of evaluating `n₁ + o₂`. Finally, `ADD2` evaluates the concrete sum in the case also the second argument evaluates to `Some` value `n₂`. The division goes straightforwardly. It only details the case of the division by 0 in the `DIV0` rule. If the second argument reduces to 0, `None` is propagated to the parent nodes in the derivation tree. In the original paper, all the `None` rules where bundled together, to reduce the number of the rules.

Similar to what we did with expression, we need to update the syntax of commands. We introduce $x :=_1 o$ as an intermediate stage for the assignment evaluation, $r;_1 c_2$ for command sequencing, and `if1` for the `if-else` command. We do not have an intermediate stage for the `while` construct, as we do plan to evaluate it as we did in Section 1.2.1 by transforming the command into an `if`. The evaluation of the loop statement will happen following the big-step philosophy, meaning that its evaluation is contained in a single derivation tree. We present the new Backus-Naur-form syntax in Figure 1.12. Notice that we have introduced a new syntactic element, `RES`. This type defines the output sort of the new command transition relation $\Rightarrow_c$. We could have just kept going on using the option value. This change aims to mark the difference between expression and commands results. Then, in Figure 1.13, we present the pretty-big-step rules for this `while` language. Let us consider the assignment and the sequence rule set. For the assignment, the rule `ASSIGN` first evaluates the first expression to an option value `o`, then evaluates the new assignment $x :=_1 o$ in $\sigma$. Notice that after the evaluation, the assignment operator is `:=_1`, a syntactic construct made for holding option
Store × CMD ⇒<sub>c</sub> Res

SKIP
---
σ, skip ⇒<sub>c</sub> σ

ASSIGN
---
σ, e ⇒<sub>e</sub> o
σ, x :=<sub>1</sub> o ⇒<sub>c</sub> r
σ, x := e ⇒<sub>c</sub> r

ASSIGNN
---
σ, x :=<sub>1</sub> None ⇒<sub>c</sub> Exc σ

ASSIGNV
---
σ, x :=<sub>1</sub> Some v ⇒<sub>c</sub> (σ + x → v)

SEQ
---
σ, c<sub>1</sub> ⇒<sub>c</sub> r
σ, r ;<sub>1</sub> c<sub>2</sub> ⇒<sub>c</sub> r
σ, c<sub>1</sub> ; c<sub>2</sub> ⇒<sub>c</sub> r

SEQN
---
σ, Exc σ' ;<sub>1</sub> c<sub>2</sub> ⇒<sub>c</sub> Exc σ'

SEQ1
---
σ', c<sub>2</sub> ⇒<sub>c</sub> r
σ, σ' ;<sub>1</sub> c<sub>2</sub> ⇒<sub>c</sub> r

IF
---
σ, e ⇒<sub>e</sub> o
σ, if1(o){c<sub>1</sub>}else{c<sub>2</sub>} ⇒<sub>c</sub> r
σ, if(e){c<sub>1</sub>}else{c<sub>2</sub>} ⇒<sub>c</sub> r

IFN
---
σ, if1(None){c<sub>1</sub>}else{c<sub>2</sub>} ⇒<sub>c</sub> Exc σ

IFT
---
σ, c<sub>1</sub> ⇒<sub>c</sub> r
σ, if1(Some T){c<sub>1</sub>}else{c<sub>2</sub>} ⇒<sub>c</sub> r

IFF
---
σ, c<sub>2</sub> ⇒<sub>c</sub> r
σ, if(Some F){c<sub>1</sub>}else{c<sub>2</sub>} ⇒<sub>c</sub> r

WHILE
---
σ, if(e){c; while(e){c}}else{skip} ⇒<sub>c</sub> r
σ, while(e){c} ⇒<sub>c</sub> r

<caption>Figure 1.13: Commands Evaluation in Pretty-Big-Step</caption>

values instead of expressions, allowing for analyzing the expression evaluation result. Moreover, the result *r* of $σ, x :=<sub>1</sub> o ⇒<sub>c</sub>$, is the overall result of the assignment. Then, if *o* is a None result, the overall result *r* is an exception *Exc σ* (rule ASSIGNN). Otherwise, we update *σ* with the new binding. The result *r* is (*σ* + *x* → *v*). For the sequence command, the approach is quite similar. Similarly, we also have one more sequence construct ;<sub>1</sub> for analyzing the intermediate results of evaluating the first sequenced command $c_1$. Notice that if the evaluation of $c_1$ is an exception, this is propagated (rule SEQN). Otherwise, *r* is a store $σ'$. The rule SEQ1 evaluates in *σ* the syntactic construct $σ' ;<sub>1</sub> c_2$. The store $σ'$ is the new sigma propagated by *r*, which has to be used for evaluating $c_2$. Indeed, $σ'$ results from evaluating $c_1$ in *σ*, while *σ* is the initial store. This process of updating the store can be related to standard monadic techniques that propagate
implicitly updated information to some construct's continuation.
# THE SKEL SPECIFICATION LANGUAGE

## Contents

<table><tr><td>2.1 The Skel Language</td><td>28</td></tr><tr><td>2.1.1 An Arithmetic Language in Skel</td><td>29</td></tr><tr><td>2.1.2 The Necro Ecosystem</td><td>32</td></tr><tr><td>2.1.3 An Interpreter for The Arithmetic Language</td><td>36</td></tr><tr><td>2.2 Related Specification Language</td><td>39</td></tr><tr><td>2.3 Conclusion</td><td>41</td></tr></table>

> « If you cannot get rid of the family skeleton,
> you may as well make it dance. »

> - George Bernard Shaw

## Introduction

In the previous chapter, we presented different semantic styles for formally encoding the behavior of programming languages. In this chapter, we move the focus to the meta-languages used to capture semantics.

Section 2.1 informally introduces the meta-language Skel, a tiny functional specification language for writing Skeletal Semantics [8], by presenting, in Section 2.1.1, a minimal arithmetic language written in this language. Then, in the following section (Section 2.1.2), we broadly present necro, a set of tools designed for generating artifacts from a Skel mechanization. In the section, we overview the entire necro ecosystem, focusing on the generation of OCaml interpreters from a Skel. Afterward, in Section 2.1.3 we present an OCaml instantiation of an interpreter for the arithmetic language.
$$
\begin{align*}
\mathit{eval_stmt}(\sigma, \mathit{While}(e, t)) &:= \\
& \quad \mathit{let} \ b = \mathit{eval_expr}(\sigma, e) \ \mathit{in} \\
& \quad \left( \begin{array}{@{}l@{}}
    \mathit{let} \ \mathit{True} = b \ \mathit{in} \ \mathit{let} \ \sigma' = \mathit{eval_stmt}(\sigma, t) \ \mathit{in} \\
    \phantom{\mathit{let} \ \mathit{True} = b \ \mathit{in} \ } \mathit{eval_stmt}(\sigma', \mathit{While}(e, t)) \\
    \mathit{let} \ \mathit{False} = b \ \mathit{in} \ \sigma
  \end{array} \right)
\end{align*}
$$

<caption>Figure 2.1: skeleton for the While constructor</caption>

We conclude the chapter by presenting an overview of related specification lan-
guages. The following chapters will discuss the limitations and differences between
these works and Skel, accordingly to the purpose of the chapter.

This chapter contains introductory material [53, 41], which are not contributions of
the author. Nevertheless, works presented in the thesis helped to refine the Skeletal
Semantics formalism and the Skel language.

2.1 The Skel Language

Skeletal semantics is a syntax to define the semantics of programming languages
in a concise yet powerful way, with a light formalism. This provides a way to easily
manipulate the semantics, for instance to convert it into a Coq formalization or an
OCaml interpreter. One of the strengths of Skeletal Semantics is the possibility to leave
some constructions undefined, to let them be implementation dependent or for gradual
specification. The theoretical concept behind Skeletal Semantics was presented in [8],
and summarized in this thesis in the background chapter.

The "Skel" language, which has been defined to describe skeletal semantics, serves
as support for the necro ecosystem [51], which provides, among other things, a genera-
tor of OCaml interpreters [42], a generator of gallina formalization [50], and a debugger
generator [49].

The Skel formalization of the semantics of JavaScript internal algorithms presented
in Chapter 4—which constitutes a main contribution of this thesis—has led us to propose
several improvements to Skel, such as writing a functional meta-language provided
with polymorphism and first-class functions.
Figure 2.1 shows an example of a skeleton for the evaluation of a *while* block of a vanilla while language in big-step style. We see all the main elements of Skeletal Semantics and we can observe that they are actually the main elements of any semantics.

* Recursion (`eval_stmt` and `eval_expr`) lets us define the semantics depending on the semantics of other terms (frequently subterms, but not always, as we can see in this example with the call `eval_stmt (σ', While (e, t)))`).

* There are auxiliary functions and auxiliary types such as booleans, and possibility to match a variable against a given constructor (e.g True).

* The `let...in` construct is used to perform a sequence of operations.

* The branching (represented as a parenthesized system in Figure 2.1) is a choice between two possible rules. Often, the branches are mutually exclusive and a pattern matching at the start of the branch determines which branch is taken. Non-mutually exclusive branches also let us represent non-deterministic semantics (such as λ-calculus with no evaluation strategy).

## 2.1.1 An Arithmetic Language in Skel

We first present a simple arithmetic language in Skel. We keep the language simple, without introducing side effects, as the purpose of this section is to practically introduce, and show how to define semantics in Skel. Afterward, we will show how to generate an OCaml interpreter via `necroml` tool.

### 2.1.1.1 Syntax and Semantics

Consider the simple arithmetic language defined in Figure 2.2. We now describe its specification in Skel, depicted in Figure 2.3. First, the set $N$ of natural numbers is required. As we do not want to specify this set in Skel, we simply state it exists using the *unspecified type declaration type nat*. Next, the syntax of terms needs to be given. To this end, we provide a *specified type declaration* in the form of an algebraic data type *term* with three constructors: `Const` taking a nat, and `Add` and `Sub` taking a tuple of two expressions.
Abstract syntax of the Arithmetic Language

$$
\mathbf{NAT} \quad n \in \mathbb{N}
$$

$$
\mathbf{EXPR} \ e ::= n \mid (e_1 + e_2) \mid (e_1 - e_2)
$$

$$
\mathbf{VALUE} \ v ::= n
$$

Expr ⇓ Value

$$
\frac{\text{CONST} \quad \frac{e_1 \Downarrow n_1 \quad e_2 \Downarrow n_2 \quad \mathbf{add}(n_1, n_2) = n}{(e_1 + e_2) \Downarrow n} \quad \text{ADD}}{\text{n} \Downarrow \text{n}}
$$

$$
\frac{e_1 \Downarrow n_1 \quad e_2 \Downarrow n_2 \quad \mathbf{sub}(n_1, n_2) = n}{(e_1 - e_2) \Downarrow n} \quad \mathbf{SUB}
$$

<caption>Figure 2.2: Arithmetic Language</caption>

We now turn to the evaluation of this small language. First, we define the type of
values as a specified type *value* with a single constructor **Nat** taking a *nat*. To define
the evaluation of addition and subtraction expressions, we need to be able to actually
compute them on integers. As integers are unspecified in our semantics, we assume
the existence of *unspecified terms* **add** and **sub** by only giving their types. Finally, we
can give the formalization of the **↓** relation as the *specified term* **eval**, on the bottom of
Figure 2.3. This specified term takes an expression **e** as input and it returns a value. As
there are three rules to define the evaluation of arithmetic expressions, we correspond-
ingly have three branches, introduced using the **branch** ... **or** ... **or** ... **end** con-
struct. Each branch starts with a pattern matching using a let binding, such as
*let* **Const** **n** = **e** *in* ... This construct only computes if **e** has the shape **Const** **n**
for some *m*, and if so the continuation of the let binding is evaluated, with **n** bound to
*m*. If **e** does not have this shape, then the branch cannot be taken. The *let* construct
is also used for sequencing. Let us consider the second branch. First, **e** is checked to
have the shape **Add**(*e*1, *e*2), then *e*1 is recursively evaluated, and the result must be
of the form **Nat** **n**1. Note that defined terms are by default recursive. Similarly, *e*2 is
recursively evaluated to **Nat** **n**2. Both numbers are added using the unspecified term
type nat

type expr =
| Const nat
| Add (expr, expr)
| Sub (expr, expr)

type value = | Nat nat

val add : (nat,nat) → nat

val sub : (nat,nat) → nat

val eval : (e:expr) : value =
  branch let Const n = e in Nat n
  or
    let Add (e1,e2) = e in
    let Nat n1 = eval e1 in
    let Nat n2 = eval e2 in
    let n = add(n1,n2) in Nat n
  or
    let Sub (e1,e2) = e in
    let Nat n1 = eval e1 in
    let Nat n2 = eval e2 in
    let n = sub(n1,n2) in Nat n
end

<caption>Figure 2.3: Arithmetic Language Definition in Skel</caption>

add and the final result is returned, wrapped in the Nat constructor.

To sum up, a skel program is a list of type declarations, either unspecified or specified (by giving its constructors), and a list of term declarations, also either unspecified and containing only a name and type, or specified with an additional term. The possibility to declare non-specified types and terms is a really powerful tool. When defining a semantics, we sometimes do not want to go into details on how every type and every function works, or we want to delay giving the actual specification to a later iteration of the design of the semantics. Partial specifications allow for that.

In the next subsection we show practically how to instantiate the artifact generated
by first presenting necroml tool, and afterwards showing how to produce a working
interpreter.
<figure><img src="image_17.png" /><figcaption>Figure 2.4: The Necro ecosystem.</figcaption></figure>

## 2.1.2 The Necro Ecosystem

The Skel language by itself is a syntax for describing abstractly programming language semantics. The library `necrolib` and the set of tools `necrotrans`, `necroml`, `necrocoq`, and `necrodebug` are built for deriving machine-executable artifacts. In this section, we present both the library and the tools. We will focus more on the `necroml` because it is the main tool used in the thesis, as it allows us to extract an OCaml interpreter module. We show the necro tools pipeline in Figure 2.4.

**necrolib** It is the main library supporting the necro ecosystem. The `necrolib` generates a `.cma` OCaml library file, providing a parser, a typechecker, and a series of pretty printers to build and print the Skel abstract syntax tree (AST). The Skel language definition is small, consisting of almost 110 LOC. The size of the language allows us to easily define a suite of tools for manipulating Skel's AST, generating artifacts in different languages.

**necrotrans** This tool is a part of the `necrolib` library. As the concrete Skeletal Semantics language is defined to support heavy use of monadic annotations, this tool is a transformer that, given a Skel file, expands all the binder-like function applications in the semantics.
necroml The tool is a generator of OCaml interpreters that, given a Skeletal Semantics .sk file, produces an OCaml functor representing its concrete semantics. The functor expects an implementation of unspecified types and terms. Once these are defined, the result is a working interpreter.

As the Skel language differs from OCaml, i.e., the *branch* is a non-deterministic construct representing different computation pathways, the produced artifact is a Skel shallow embedded in the OCaml's framework only for the unspecified types and terms. The behaviour of skeletons is defined by interpretation monads that declare how each skeleton is concretely computed. This choice fits with the theoretical framework itself, as the *branch* non-determinism allows to collect all the possible valid computations.

Executing the tool generates an OCaml file with 4 module types (*TYPES*, *MONAD*, *UNSPEC*, *INTERPRETER*) and two functors (*Unspec*, *MakeInterpreter*) to be implemented.

The module *TYPES* defines the names of all the unspecified types defined in the original .sk file. In this case, a user has to provide a module with a concrete type implementation.

The module *MONAD* represents the interpretation monad, explaining how the skeletons are concretely evaluated. Naïvely, a user can define a Skeletal Semantics identity monad. In Figure 2.5, on the top listing, we show the interpretation monad module type and its implementation on the bottom.

In this case, branches (*branch* function) are evaluated sequentially, considering the first successful branch as the branch to continue to evaluate. It is the closest approach to a shallow embedding in OCaml, separating the logics of Skeletal Semantics from the OCaml one. The problem with this implementation of the ID monad is that in case of future failures, it is impossible to backtrack and choose another branch if any. The *bind* and *apply* terms are pretty similar, but the first is the binder for the *let-in* skeleton, binding a fully evaluated term *t* to a variable *x*, in the environment of the continuation. The *apply* is the concrete term application used while evaluating the OCaml code. We can resume the differences with an example showing the generated code. Given a Skel snippet of code, `let r =@ f x in (*B*)`, where *f* is a higher-order term defined in the formalization of type `'a -> 'b`, representing a continuation, *x* a variable name or a formalization value of type `'a`, and `@` is a binder named "*id_bind*" defined in the skeletal semantics, the generated code can be represented compactly in the following listing.
```hkl
module type MONAD = sig
  type 'a t
  val ret: 'a -> 'a t
  val bind: 'a t -> ('a -> 'b t) -> 'b t
  val branch: (unit -> 'a t) list -> 'a t
  val fail: string -> 'a t
  val apply: ('a -> 'b t) -> 'a -> 'b t
  val extract: 'a t -> 'a
end
```

```hkl
module ID = struct
  exception Branch_fail of string
  type 'a t = 'a
  let ret x = x
  let bind x f = f x
  let rec branch l =
    begin match l with
      | [] -> raise (Branch_fail "no match")
      | bh::bt -> try bh () with Branch_fail _ -> branch bt
    end
  let fail s = raise (Branch_fail s)
  let apply f x = f x
  let extract x = x
end
```

<caption>Figure 2.5: The interpretation monad module and its identity monad instantiation</caption>

```hkl
let* _tmp = apply1 f x in
apply2 id_bind _tmp (function r -> (*B*))
```

The operator `let*` and the functions `apply1` and `apply2` are respectively defined as:
```hkl
let ( let* ) = M.bind
let apply1 = M.apply
let apply2 f arg1 arg2 =
    let* _tmp = apply1 f arg1 in
    apply1 _tmp arg2
```

The generated code can be presented extensively as shown below.

```hkl
M.bind (M.apply f x)
    (λ _tmp -> M.bind (M.apply id_bind _tmp)
     (λ _tmp1 -> M.apply _tmp1
      (function r -> (*B*) ))))
```

Notice that the result of `f x` is encapsulated in the skeletal semantics interpretation monad. So concretely, `f`'s signature is defined as `'a -> 'b t` as the skeletons evaluation is monadic. Hence term evaluation is encapsulated in skeletons monad. The variable `_tmp` is a temporary variable name holding a computation result of `f` applied to `x`.

The `fail` and `extract` terms respectively return an error message and extract values from the interpretation monad, usually the computation result. In the `necrolib` library, there are already some predefined interpretation monads, each providing Skeletal Semantics with a different meaning<fnref n="1" />.

The module type `UNSPEC` contains all the types of the original `.sk` file, the unspecified terms signature, and the interpretation monad. The interpretation monad is present because it can influence the definition of unspecified terms.

Finally, the `INTERPRETER` module type defines the signatures of all the interpreter's types and terms. It is an extension of the module `UNSPEC`, containing the definition of the specified terms (the formalization).

Then, regarding the two functors, the `Unspec`, given an instantiation of the module `TYPES` and the interpretation monad instantiations as parameters, produces a concrete instantiation of the module `UNSPEC`. Notice that undefined unspecified terms return a `NotImplemented` result by default, and the actual implementation can overwrite their

<footnote n="1">1. Concrete implementation of the default interpretation monads in https://gitlab.inria.fr/skeletons/necro-ml/-/blob/FSCD2022/necromonads.ml</footnote>
definitions. Then, the functor `MakeInterpreter` takes the instantiations of unspecified types and terms (the `Unspec` functor) and produces the interpreter for the formalization.

**necrodebug** The necro ecosystem also comprehends a debugger, very useful when writing big formalizations. The tool is an OCaml debugger generator, which given the Skel formalizations and a program that is written according to the formal syntax defined in the Skel file, it produces a step-by-step execution file using an abstract machine interpretation of Skel. The debugger provides two user interfaces, a terminal, and an HTML page generated by `js_of_ocaml`. An instantiation is needed to execute the debugger, similarly to the `necroml`. Actually, the same instantiation can be used both for the interpreter and the debugger. Then, the debugger needs to be extended by a suite of pretty printers.

**necrocoq** The `necrocoq` tool generate a deep embedding coq formalization from a Skel file. The produced artifact can be used to prove a program to be correct, or to validate properties of the programming language semantics itself, e.g. properties of the semantics of JavaScript.

### 2.1.3 An Interpreter for The Arithmetic Language

Once the skeletal semantics of the arithmetic language is defined, as presented in Figure 2.3 in a file `.sk`, an artifact can be produced with the `necroml` tool.

**The TYPES module type** This module is a list of declarations of unspecified types. In the Skel code, only the `nat` type has been left unspecified. We say that the naturals are the OCaml integers, defining the Skeletal type in the host language concrete definition of these numbers. We show the generated module and its instantiation in the listing below.
```pascal
(* Generated module TYPES *)
module type TYPES = sig
  type nat
end
```

```pascal
(* Custom implementation *)
module Types : sig
  type nat = int
end = Types
```

### The UNSPEC module type
This module is parametrized by a functor that provides default atomic definitions of the unspecified terms and the implementation of the specified terms and types. The `necroml` tool produces the following module type and functor.

In the top listing of Figure 2.6, the module `UNSPEC` presents the signature of the terms `add` and `sub`. In the central listing of Figure 2.6, we show the default functor `Unspec`. Each unspecified term has a default implementation that returns a `NotImplemented` result. In the bottom of Figure 2.6, we show the customized implementation of both these terms.

Notice that the interpretation monad, the `ID` monad shown in Figure 2.5, and the functor `Types` are included for instantiating the module `Unspec`. The `Types` module provides a concrete meaning to the unspecified type `nat`.

### The INTERPRETER module type
This module is a declaration of all the terms and types, either specified or non-specified. This module declares the signatures of all the interpreter components, and it is instantiated by the functor `MakeInterpreter`. The result of the generation is presented in Figure 2.7: on the top, we have the module type declaration, and on the bottom, the functor. The functor provides an implementation to the specified terms definition signatures defined on the left listing, a shallow embedding of the Skeletal Semantics language definition. Hence, by providing the `Unspec` functor as an argument to the `MakeInterpreter` one, one can produce a real interpreter for the arithmetic language.

```python
module Interp = MakeInterpreter(Unspec)
```
(* Generated Module Type *)
module type UNSPEC = sig
  module M: MONAD
  include TYPES
  type value = | Nat of nat
  and expr = | Sub of (expr * expr) | Const of nat
  | Add of (expr * expr)
  val add: nat*nat ->nat M.t
  val sub: nat*nat ->nat M.t
end

(* Generated Default Functor *)
module Unspec (M: MONAD)(T: TYPES)=struct
  exception NotImplemented of string
  include T
  module M = M
type value = | Nat of nat
  and expr = | Sub of (expr * expr) | Const of nat
  | Add of (expr * expr)
  let add _ = raise(NotImplemented "add")
  let sub _ = raise(NotImplemented "sub")
end

(* Custom Implementation *)
module Unspec = struct
  include Unspec(ID)(Types)
  let add ((a,b) : (nat*nat)) : nat M.t = M.ret (a + b)
  let sub ((a,b) : (nat*nat)) : nat M.t = M.ret (a - b)
end

<caption>Figure 2.6: The UNSPEC module type and its functors.</caption>

Then a program can be written and executed. For example, the program 1 + 1 - 2
can be encoded and executed by writing this code.

open Unspec
open Interp

let _ = M.extract (eval (Sub (Add (Const 1,Const 1), Const (-2)))))
(* Generated Module type *)
module type INTERPRETER =
sig
  module M: MONAD
  type nat
  type value = | Nat of nat
  and expr = | Sub of (expr * expr) | Const of nat
  | Add of (expr * expr)
  val add: nat*nat-> nat M.t
  val eval: expr-> value M.t
  val sub: nat*nat-> nat M.t
end

(* Generated Functor *)
module MakeInterpreter (U: UNSPEC)=
struct
  include U
  let ( let* ) = M.bind
  let apply1 = M.apply
  let rec eval e =
    begin match e with
      | Const n -> M.ret (Nat n)
      | Add (e1, e2) ->
        let* Nat n1 = apply1 eval e1 in
        let* Nat n2 = apply1 eval e2 in
        let* n = apply1 add (n1, n2) in
        M.ret (Nat n)
      | Sub (e1, e2) -> ...
    end
end

<caption>Figure 2.7: The INTERPRETER module type and its functor.</caption>

## 2.2 Related Specification Language

In the thesis, we present all the formalizations in Skel by presenting the behavior formally as an inference rule set or some algorithmic steps (in Chapter 4), then show how to encode them in our language.

To resume, Skel is the language for writing Skeletal Semantics, supported by necro, a library with a tool suite for manipulating the AST and producing different artifacts. We structure this section by presenting in each paragraph a different framework without
digging into which is better and why. We leave it to the following chapters. Generally, the evaluation we make is in terms of conciseness, closeness to the formal or informal definition of the language, and maintainability, which we think is crucial if we want to support work over the years when new releases of languages come out.

The properties of Skel rely upon the complexity of the language itself. It is a really tiny language. As shown in Chapter 1 a formal definition of a language defines the behavior of a language abstractly by defining premises that an evaluating configuration must satisfy. The operations held in the premises are usually not defined. For example, the addition relies on its natural meaning.

Considering the division we present in Figure 1.10, we explicitly write the number 0 in the Div rule, in its decimal form. Nevertheless, we could have chosen other ways to encode that number—hexadecimal, binary. A rule is just an abstraction of a behavior, decoupled from the concrete meaning of data.

In the Skel language, we can write partial specifications by defining unspecified types and terms without actual implementation.

Moreover, the language does not have native types except for user-defined constructed types. The unspecified types allow for being abstract enough not to sacrifice the readability of the semantics for constraints dependent on types. Indeed, it can be as abstract as an inference rule by only declaring unspecified components of the semantics. Then, the language is tiny, making the language prone to be used for generating artifacts of different nature. The Skel language definition stays in a couple of hundreds of lines.

In the following paragraphs, we briefly introduce the frameworks related to the thesis' contribution.

**Lem** Lem [55, 47] is a specification language allowing to extract from the source file an OCaml interpreter and mechanizations in a proof assistant framework, namely Coq and Isabelle/HOL. The scope of this specification language is vast, spreading from communication protocols to weak memory models. The language itself is complex, allowing complex type inference and constructed modules, making the overall language quite heavy to manipulate. The language has native types, such as four number types, and strings.

**Ott** Ott [66] is a tool for specifying programming languages, allowing to extract from an Ott source file a LATEX representation, Isabelle/HOL, and Coq files, and an exe-
cutable OCaml file. It also provides ways to derive a Lem mechanization. This tool is
known for its writing style, which is close to the handwritten inference rules.

K K [63] is a formal framework for writing executable semantics in a rewriting style. The framework is designed to define modular semantics in its components, such as the state. The K framework has a steep learning curve, making it quite difficult to approach. Nevertheless, many applications came from this framework, for example formalizations of JavaScript [56], C [21, 28], Java [10], and PHP [23]. Some work [17] recently provided methods for proof generation and checking in Isabelle/HOL, but, to our knowledge, no work yet provides proofs of meta-theories of a K formalization. Nevertheless, the K framework is powerful, and offers tools for analyzing K programs, such as a symbolic executor, a test-case generator, a runtime monitor, and an interpreter. This semantic framework has a Isabelle/HOL mechanization of the semantics, to formally show undesirable behaviours in the current implementations of the language [40].

## 2.3 Conclusion

In this chapter, we first presented features of the Skel language by implementing the Skeletal Semantics of a simple arithmetic language. The language can be put in the same category of semantic frameworks with Ott, Lem, and K, with the difference that Skel comes with a simple syntax and with no a priori semantics, allowing to manipulate easily a Skel AST and producing different artifacts. Afterward, we introduced tools for generating different artifacts from a Skel source. We focused more on the *necroml* tool as the thesis relates more with concrete interpretation rather than formal verification of meta-theories of a formalization. Hence, in Section 2.1.3 we showed how to generate an OCaml interpreter module of the arithmetic language, and how to instantiate it for obtaining a working interpreter.

Contributions in this thesis pushed the language to move toward a functional path. For example, representing JavaScript semantics—see Chapter 4-needed something more from the language, namely polymorphism and higher-order terms as first-class language citizens, to capture concisely and faithfully the ECMAScript specification algorithms. Skel development has been strongly influenced by the formalizations presented in the thesis.
Chapters 1 and 2 presented ways to write semantics, either on paper or on the machine, and offer the necessary knowledge to appreciate the contributions of this manuscript. The following chapters will exploit some Skel features for writing concise, modular, and executable semantics.
<figure><img src="image_18.png" /></figure>
# DESCRIBING CONCISELY EFFECTFUL SEMANTICS

## Contents

<table><tr><td>3.1</td><td>Effectful Arithmetic Language</td><td>47</td></tr><tr><td>3.2</td><td>PCF</td><td>54</td></tr><tr><td>3.3</td><td>Adding State to the PCF language</td><td>59</td></tr><tr><td>3.4</td><td>A Fully Monadic Skeletal Semantics</td><td>64</td></tr><tr><td>3.5</td><td>Explicit Contination Manipulation</td><td>69</td></tr><tr><td>3.5.1</td><td>Program Examples</td><td>70</td></tr><tr><td>3.5.2</td><td>Syntax and Semantics</td><td>71</td></tr><tr><td>3.5.3</td><td>A Stateful PCF Language with Yield and Exceptions in Skel</td><td>77</td></tr><tr><td>3.6</td><td>Related Work</td><td>81</td></tr></table>

« Je n'ai fait cette lettre-ci plus longue que parce que je n'ai pas eu le loisir de la faire plus courte. »

- Blaise Pascal [60]

## Introduction

Writing a formal definition of a programming language specification helps state precisely the behavior of the language constructs and also derive frameworks in which it is possible to prove programs and/or language properties. The result of this task must ensure that the actual semantics of the language is captured.

To ensure that a work written in a semantic framework adequately describes the meaning of the programming language, one must preserve the following properties:
1. The formalization should be textually close to the specification of the language if it exists.

2. An executable formalization should be tested against the test suite provided by the language. Thus, a suitable tool to describe semantics should make it easy to stay close to language definitions, be they algorithmic or based on inference rules, and the tool should provide a straightforward way to derive an executable version of the semantics and run code, including tests.

3. Language definitions written in such a tool should be easy to manipulate, for instance, to derive a mechanized version in a proof assistant, inspect the semantics, or transform it.

In this chapter, we define a method for structuring the semantics of a sequence toy languages written in Skel. In Section 3.1, we extend the simple arithmetic language presented in Section 2.1.1 by introducing the division and multiplication expressions, a try-catch expression, and a datatype describing the exceptions of the language. We then structure the chapter in the following way. Section 3.2 extends the effectful arithmetic language by introducing first-class functions and a fix-point operator. In Section 3.3, we continue extending this language by adding a mutable state and extending the language with some state operators. In Section 3.5, we show how to add delimited computations and explicitly handle the natural control flow of a program. We show in each section how to introduce these new features without disrupting the formalization of the constructs that do not directly use them. The final language we present is syntactically simple, but its behavior is far from trivial. We also provide the semantics and the interpreter of every language presented in the chapter in a source repository<fnref n="1" />. Finally, in Section 3.6, we relate our approach to existing work.

<footnote n="1">1. https://gitlab.inria.fr/akhayam/programming_skel</footnote>
Contribution

The chapter presents:

* a systematic approach to capture multiple side-effects in Skel formalizations.

* exploit the power of monads to write readable, and maintainable semantics in Skel.

* structurally solid evaluation functions. Extending a language by introducing new effectful operations does not impact the code describing the previously written core language.

## 3.1 Effectful Arithmetic Language

In this section, we first show how to introduce effects in Skeletal Semantics by adding the division operator to the arithmetic language presented in Section 2.1.1. The evaluation of an expression with a division can fail because of a division by 0 exception. We first try to handle effects explicitly, and then we show how a monadic approach helps to structure the language's formalization. Handling explicitly side effects is transparent but not scalable when writing a real-world programming language formalization.

If we add division to the language, a program may try to perform a division by zero. To capture this information, we introduce an exception type. This type is defined by two constructors, `Exc`, representing that the computation has failed, and `Ok`, carrying type `value`, which means that the computation is successfully calculated. This type is similar to **OCaml's** `option type` or **Haskell's** `maybe type`. We show the syntax definition of the exception type in BNF and Skel in Figure 3.1. We put in the syntax `...` for saying that there are other type constructors defined for the expression type, namely `Const`, `Add`, and `Sub`.

We present the evaluation rules of this language, inference rules, and Skel in Figure 3.2 and Figure 3.3. We omit the rules for subtraction and multiplication. First, we give an alias `type output := exc` such that the result of `eval` is always `output`, even for more complex languages (we will change the alias when needed). We
Formal Syntax

EXC o ::= Exc
| Ok v
EXPR e ::= ...
| (e₁/e₂)
| try{e₁}{e₂}

type exc = | Exc
             | Ok value

type expr = | ...
             | Div (expr, expr)
             | Try (expr, expr)

<figure><img src="image_19.png" /><figcaption>Figure 3.2: Arithmetic Language Rules Extended with Division and Exceptions</figcaption></figure>

assume two unspecified terms to test for zero and not zero and an unspecified third
term to divide two numbers. We also assume that this last unspecified term should
never be called with a divisor which is zero. We finally extend the syntax of arithmetic
expressions with a division operator and a try with construct to catch exceptions.

As there are 13 rules to evaluate arithmetic expressions with division (the three rules
```pascal
type output := exc
val zero: nat → ()
val not_zero: nat → ()
val div: (nat,nat) → nat
val mul: (nat,nat) → nat
val eval (e: expr) : output =
  branch let Const n = e in (Ok (Nat n))
  or      let Add (e1,e2) = e in
        let o1 = eval e1 in
        branch let Exc = o1 in o1
        or      let Ok (Nat n1) = o1 in
                  let o2 = eval e2 in
                  branch let Exc = o2 in o2
                  or      let Ok (Nat n2) = o2 in
                            let n = add (n1,n2) in
                            Ok (Nat n)
        end
        end
or      let Div (e1,e2) = e in
        let o1 = eval e1 in
        branch let Exc = o1 in o1
        or      let Ok (Nat n1) = o1 in
                  let o2 = eval e2 in
                  branch let Exc = o2 in o2
                  or      let Ok (Nat n2) = o2 in
                            branch zero n2; Exc
                            or      not_zero n2;
                                      let n = div(n1,n2) in
                                      Ok (Nat n)
                            end
                            end
end
or      let Try (e1,e2) = e in
        let o1 = eval e1 in
        branch let Exc = o1 in eval e2
        or      let Ok (Nat r1) = o1 in o1
        end
or
end
```

<caption>Figure 3.3: Arithmetic Language in Skel Extended with Division and Exceptions</caption>
for subtraction being omitted), one might expect 13 branches to be needed. Fortunately, Skel lets us factorize some of the behavior. Consider the case of addition: in the three rules shown, the first sub-expression is always evaluated. Hence the corresponding Skel rule also evaluates it to $o_1$, and then it branches for inspection. If it is an exception, then it is propagated. Otherwise, it is a number $n_1$, and the computation may continue with the evaluation of $e_2$. Such factorization may be compared to the one obtained using Pretty-Big Step Semantics [15], as shown in Section 1.4.

This description is still somewhat naïve because the same code structure must be repeated for division (in blue) and subtraction (not shown). Before improving the implementation, let us describe the code for division and **Try**. Regarding division, once both sub-expressions are successfully computed, the second one is tested against zero: if it is zero, an exception is raised; if it is not, the division may proceed. Once again, branches are used to capture a conditional. As branches are inherently non-deterministic, one must ensure that the required conditions are fully stated. Note that we use the syntactic sugar `foo; rest` for `let _ = foo in rest`, and rely on the partiality of the zero and not_zero unspecified terms.

Regarding the **Try** term, we first evaluate its first sub-expression. If it results in an exception, we evaluate the second sub-expression; if it succeeds, we return its value.

One may observe that adding exceptions makes the code significantly bigger and less readable, with much more of structural duplication.

To capture such effects in Skel, we rely on the classical approach of monads. As a first approximation, a monad is a triple {$M, \mathit{return}, \mathit{bind}$}, where

* $M$ is a monadic type constructor, taking a type and returning a type;

* `return : α → Mα` is a function that takes a pure value of type $α$ and returns the same value in the monad;

* `bind : Mα → (α → Mβ) → Mβ` is a function that takes $w$, a monadic value of type $α$, a continuation $f$ of type $α → Mβ$, and `bind w f` returns a new monadic value of type $Mβ$.

Monads also come with laws that state that `ret` and `bind` are inverse of each other in some sense. These laws can be ignored because we do not prove the properties of our code.

To write monads in Skel, we introduced [52] higher-order terms as first-class citizens as well as parametric polymorphism. Polymorphism is always explicit: the polymorphic
type `exc<a>` is parametric in its type parameter `a`, which can be used in its definition (as in `type exc<a> = | Exc | Ok a`). Polymorphic term declarations and polymorphic constructors also have this typesetting. Examples are the `return` and `bind` defined below.

```k
val return<a> (v:a) : exc<a> = Ok<a> v
```

```k
val bind<a,b> (w: exc<a>) (f: a -> exc<b>) : exc<b> =
    branch let Exc = w in throw<b> ()
    or let Ok v = w in f v
end
```

On the other hand, constructors used as patterns do not require polymorphic annotations as they can be locally inferred.

These three declarations actually form the exception monad that we use in Figure 3.4. They include an additional return always to throw and functions specialized to the value type (to avoid annotations). We do not include the `return` and the `bind` function in the figure.

In the same figure, below, we give the `eval` function using the exception monad. As the `bind` function expects a function as a second argument, and as we prefer to avoid defining such functions as top-level terms, we introduce a final part of Skel's syntax: anonymous functions. They are simply written `λp:t → s`, where `p` is a pattern, `t` is a type, and `s` is a skeleton. We thus give as a continuation of each `bind` the remainder of the code, and there is no need to branch on the status of an evaluation to decide whether to continue or throw, as the `bind` takes care of it.

To make the code more readable, we make the use of `bind` for continuation code more straightforward. We declare that the higher-order term is a `bind` and assign it a symbol by writing `binder @ := bind`. When this is done, code like `bind o (λ(x:t) → s)` can simply be written `let x =@ o in s` (type annotations are inferred). The resulting code is shown in Figure 3.5. We can even abuse this notation to define another `bind`-like function `exccont`, which calls its continuation in the case an exception was raised and otherwise return the given value to give it a symbol and use it in the code for `Try`. We associate this behavior with the symbol `?`, which represents the monadic term `exccont`. If this code, the construct `e1; e2`, stands for `let _ = e1 in e2`, then `eval e1;? eval e2` states evaluating `e1`, if it returns an exception, then evaluate `e2`,
```h
val throw<a> (_:) : exc<a> = Exc<a>
```

```h
type output := exc<value>
```

```h
val ret (v:value) : output = return<value> v
```

```h
val thr (_:) : output = throw<value> ()
```

```h
val eval : (e:expr) -> output
```

```h
branch let Const n = e in ret (Nat n)
```

```h
or let Div (e1,e2) = e in
```

```h
let o1 = eval e1 in
```

```h
bind<value,value> o1 (\v1:value ->
```

```h
let Nat n1 = v1 in
```

```h
let o2 = eval e2 in
```

```h
bind<value,value> o2 (\v2:value ->
```

```h
let Nat n2 = v2 in
```

```h
branch let _ = zero n2 in
```

```h
thr ()
```

```h
or not_zero n2;
```

```h
let res = div(n1,n2) in
```

```h
ret n
end))
```

```h
or let Add (e1,e2) = e in
```

```h
let o1 = eval e1 in
```

```h
bind<value,value> o1 (\v1:value ->
```

```h
let Nat n1 = v1 in
```

```h
let o2 = eval e2 in
```

```h
bind<value,value> o2 (\v2:value ->
```

```h
let Nat n2 = v2 in
```

```h
let n = add(n1,n2) in
```

```h
ret n))
```

```h
or ...
```

```h
end
```

<caption>Figure 3.4: Exception monad in Skel, and its application to the eval function</caption>

otherwise return its result. Introducing a symbol for a bind operator is not required; one
may directly use the notation `let x =%bind o in s` to stand for `bind o (\lambda x -> s)`. In
the following listing, we show the implementation of the function `exccont`.
```hsl
val eval (e: expr) : output
    branch let Const n = e in ret (Nat n)
    or      let Div (e1,e2) = e in
            let Nat n1 =@ eval e1 in
            let Nat n2 =@ eval e2 in
            branch zero n2; thr ()
            or      not_zero n2;
                      let n = div(n1,n2) in
                      ret (Nat n)
        end
    or      let Try (e1,e2) = e in
            eval e1;?
            eval e2
    or      let Add (e1,e2) = e in
            let Nat n1 =@ eval e1 in
            let Nat n2 =@ eval e2 in
            let n = add(n1,n2) in
            ret (Nat n)
    or      ..
end
```

<caption>Figure 3.5: Exception Monad and its Symbolic Application to eval</caption>

```hsl
val exccont<a> (v:exc<a>) (f:() -> exc<a>): exc<a> =
    branch let Exc = v in f ()
    or      let Ok v' = v in
            return<a> v'
end

binder ? := exccont
binder @ := bind
```

In this subsection, we showed how to extend a language in Skel, introduced monads and binders, and used them. We defined a writing pattern that makes the semantics highly readable and compact.
```haskell
let zero (a:nat) : unit M.t =
match a with
| 0 -> M.ret ()
| _ -> M fail "not zero"
```

<caption>Figure 3.6: The zero term implementation</caption>

### Instantiation

To instantiate an interpreter to the language presented in this section, a user can simply, after a `necroml run`, extend or include the `Unspec` functor shown in Figure 2.6. We provide an implementation to the unspecified terms `zero`, `not_zero`, `div`, and `mul`. Note that the `zero` and the `not_zero` terms are partial functions. These function may fail in the Skel interpretation monad. We show the implementation of the `zero` term in Figure 3.6.

### Remark

We remark that the monads we present in this semantics are not related to the interpretation monads of the ml-instantiation. The monadic approach we present represents the way we write semantics.

## 3.2 PCF

Even with exceptions, a language for arithmetic expressions is still far from an actual programming language. We thus extend it with variables, first-class functions, a sequencing operator, `skip`, and a fix-point operator.
Formal Syntax

...
ENV $\sigma$: VAR $\to$ VALUE
VAR $x \in \Sigma^+$
VALUE $v ::= n$
  | $(x, t_x, \sigma_{cl})$
  | $(x, t_x, \sigma_{cl}, x_f)$
  | ()
EXPR $e ::= ...$
  | $x$
  | $\lambda x.e_x$
  | $e_1 e_2$
  | `let x = e_x in e_c`
  | `if0(e_c){e_1}{e_2}`
  | `fix fx.e_x | e_1; e_2`
  | `skip`

...
**type** env
**type** var
**type** value =
  | **Nat** nat
  | **Clos** (var, expr, env)
  | **ClosRec** (var, expr, env, var)
  | **Unit**
**type** expr =
  | ...
  | **Var** var
  | **Lam** (var, expr)
  | **App** (expr, expr)
  | **LetIn** (var, expr, expr)
  | **If0** (expr, expr, expr)
  | **Fix** (var, var, expr)
  | **Seq** (expr, expr)
  | **Skip**

The evaluation of this language requires an environment $\sigma$: VAR $\to$ VALUE that maps variables to values. We define the semantic judgement as $\sigma, e \Downarrow$ Exc Value. In the arithmetic language, Nat was the only possible value. In PCF, we add the unit value and closures. The value unit represents a singleton value we use to return no value. Then, we define two types of closures. The first type represents the result of evaluating a lambda expression, and this value stores the bound variable x, the body of the abstraction eb, and the current environment s as Clos ($x, eb, s$). The second type of closure represents recursive closed expressions. Similarly to the non-recursive closure, the recursive one stores x, eb, s, and the name of the recursive expression f as ClosRec ($x, eb, s, f$). The environment must specify which values the free variables of eb are bound to.

The presence of an environment to evaluate an expression means that the eval function must change its signature: it now takes both an environment and an expres-
sion. The output of this function is a value in the exception monad. The evaluation is
shown in both Figure 3.7 and Figure 3.8. The case of arithmetic operations is un-

<figure><img src="image_20.png" /><figcaption>Figure 3.7: PCF Semantic Rules</figcaption></figure>

changed, except for adding the environment to the recursive call of eval. Variables are
looked up in the environment. The evaluation of an application App(e1, e2) in the en-
```pascal
val eval (s:env) (e:expr) : output =
    branch ...
or      let Add (e1,e2) = e in
          let Nat n1 =@ eval s e1 in
          let Nat n2 =@ eval s e2 in
          let n = add(n1,n2) in ret (Nat n)
or      let Var x = e in
          let v = getEnv s x in ret v
or      let Lam (x,ex) = e in
          ret (Clos (x,ex,s))
or      let App (e1,e2) = e in
          let cl =@ eval s e1 in
          let w =@ eval s e2 in
      branch let Clos (x,eb,sc) = cl in
          let sc' = extEnv sc x w in
          eval sc' eb
      or      let ClosRec (x,eb,sc,f) = cl in
          let sc' = extEnv sc x w in
          let sc'' = extEnv sc' f cl in
          eval sc'' eb
end
or      let LetIn (x,ex,ec) = e in
          let vx =@ eval s ex in
          let s' = extEnv s x vx in
          eval s' ec
or      let IfO (ec,e1,e2) = e in
          let Nat nc =@ eval s ec in
      branch zero nc; eval s e1
          or      not_zero nc; eval s e2
      end
or      let Fix (f,x,ex) = e in
          ret (ClosRec (x,ex,s,f))
or      let Seq (e1,e2) = e in
          eval s e1 ;@
          eval s e2
or      let Skip = e in ret Unit
end
```

<caption>Figure 3.8: PCF Semantics in Skel</caption>
```h
let extEnv (e:env) =
    M.ret (fun x -> M.ret (fun v -> M.ret (SMap.add x v e)))
```

<caption>Figure 3.9: extEnv instantiation in OCaml</caption>

vironment s first evaluates e1 in s. The result must be a closure `Clos(x, ex, sc)` or a recursive closure `ClosRec(x, ex, sc, f)`. The argument e2 is then evaluated in s to w. Finally, the body of the closure ex is evaluated in the environment sc extended with a mapping from x to v. In the recursive case, sc is also extended with a binding from f to `ClosRec(x, ex, sc, f)`. Note that these steps are done in the exception monad: once one evaluation returns an exception, it is propagated, and the evaluation is interrupted.

We assume that all the arithmetic operations, including multiplication, are described by our semantics, so in the figure, we show only the evaluation steps for the `Add` constructor. We use integers for conditionals with the `If0` operator.

To access and extend the (unspecified) environment, we assume the existence of the `getEnv` and `extEnv` terms. The environment is assumed to be a partial mapping from `VAR` to `VALUE`. In case a mapping does not exist, the result of getting a variable's value is a Skel failure. Indeed, we decided not to capture it in the exception monad to be consistent with other errors, such as applying a number as a function. These errors could be detected statically by writing a PCF type checker.

Figure 3.8 shows the new `eval` function for PCF in Skel. The evaluation of the language is almost standard. The rules follow the ones from [62] with two exceptions: we use an environment instead of substitution and provide a big-step semantics. Because of the former, the `Fix` operator's semantics is described as follows. `Fix(f, x, ex)` is evaluated to a recursive closure `ClosRec(x, ex, sc, f)`, which is a value. The extension of the environment with f bound to the recursive closure is delegated to the application if it happens. Notice that this evaluation is close to the evaluation of a `λ`-expression. A PCF program defining and using factorial can be written as follows, in concrete syntax (in Skel, we would need to use the constructors `LetIn`, `Fix`, etc.)

```h
let fact = fix factrec n. if0(n) {1} {n*(factrec (n-1))} in
fact 42
```
## Instantiation

To generate an interpreter, one must extend the Types functor providing a concrete type to variables and the environment $\sigma$. Moreover, The Unspec functor needs a definition for the functions getEnv and extEnv. We provide a demonstrative implementation of the extEnv in Figure 3.9. The SMap functor represents the library to manipulate maps from strings to values. The functor is constructed with the following code, `module SMap = Map.Make(String)`, and the `type env` is defined as `Unspec(M)(Types).value SMap.t`, a map from strings to the language value type defined in Skel.

## 3.3 Adding State to the PCF language

We now extend our language with a state and references. Allocating a new reference with the operator `&v` consists of extending a state $\mu$ with a new memory location $l$ containing an initial value $v$. We write the semantic judgement a $\mu, \sigma, e \downarrow$ (Exc Value, $\mu$). We define two other operations, `!l` for accessing the contents of a location $l$ (dereferencing), and the infix operator $l := v$ for setting a new value $v$ in an existing allocated location $l$. Formally, we can extend the syntax as follows.

### Formal Syntax

```
...
LOC l
STATE μ : LOC → VALUE
VALUE v ::= ... | l | ()
ST(α) st ::= μ → (α, μ)
EXPR e ::= ... | &e | !e | e₁ := e₂
```

```
...
type loc
type value = | ...
               | Loc loc
               | Unit
type state
type st<a> := state → (a,state)
type expr = | ... | Ref expr
            | Get expr
            | Set (expr,expr)
```

In Skel, we extend the value type with a `Loc` constructor for location values and
**Unit.** We leave the `loc` and `state` types unspecified and define the monadic state type (`type st<a>`). Finally, we extend `expr` type with three new language constructors: `Ref` for `&`, `Get` for `!`, and `Set` for the infix operator `:=`.

To describe the semantics, we extend our monad to include a state monad. A computation in a state monad is a function that expects the current value of the state to return its result alongside the updated state. We first define the state bind operator `stbind`, denoted with `@m`. This binder is the regular state binder.

```haskell
val stbind<a,b> (v:st<a>)(f:(a -> st<b>)) : st<b> =
    λ s : state -> let (v',s') = v s in f v' s'
binder @m := stbind
```

Next, we combine the state and exception monad, writing its `bind` operator, denoted with `@`. The monadic type considered is `v:st<exc<a>>`. It means that, given a state `µ`, the application `v µ` returns a tuple `(v', µ') : (exc<α>, state)`. We keep exceptions inside the state as a computation may mutate the state before throwing an exception, and this mutated state needs to be propagated. We show the new `bind` in the following snippet of code.

**Remark**

We chose to combine the state monad and the exception monad in this order to guarantee the state's persistence in case of a failure. In the example, we are interested in cumulating results, always being able, in case, to inspect the state. We define the combined monadic type as `STATE → (EXC a, STATE)`. Combining in the other way means having the following signature: `EXC(STATE → (a, STATE))`. In case of an exception, the computation loses the most updated state.
```h
val bind<a, b> (v:st<exc<a>>)(f: (a -> st<exc<b>>)): st<exc<b>> =
    let v' =@m v in
    branch let Exc = v' in throw<b> ()
    or      let Ok v'' = v' in f v''
    end
binder @ := bind
```

We update the `exccont` binder, represented as `?`, to take the monad into account. This lets us keep the `Try` case of the semantics unmodified. The update is symmetric to what did with the monadic binder.

```h
val exccont<a> (v:st<exc<a>>)(f: (() -> st<exc<a>>)): st<exc<a>> =
    let v' =@m v in
    branch let Exc = v' in f ()
    or      let Ok v'' = v' in return<a> v''
    end
binder ? := exccont
```

Finally, we redefine the `return` and the `throw` term. Here again, we inject the `exc<a>` return type into the state monad.

```h
val stret<a> (v:a) : st<a> = λ s:state → (v,s)
val return<a> (v:a) : st<exc<a>> = stret<exc<a>> (Ok<a> v)
val throw<a> (_:()) : st<exc<a>> = stret<exc<a>> Exc<a>
val ret (v:value) : output = return(value> v
val thr (_:()) : output = throw(value> ()
```

In Figure 3.10, we show the semantics of `Ref`, `Get`, and `Set` in Skel and big-step. We define three concrete atomic operations on memory: `alloc` is a function for allocating a new memory location with an initial value, `m_r` returns the value bound to a reference, and `m_w` writes a value in a location. The specified terms `newref`, `get`, and `set` are the monadic versions of `alloc`, `m_r`, and `m_w`. We show them below.
$$ \mu, \sigma, e \Downarrow (\mathbf{Exc} \ \mathbf{Value}, \mu) $$

$$ \frac{\text{REF} \qquad \mu, \sigma, e_r \Downarrow (\mathbf{Ok} \ v, \mu'') \qquad \text{alloc}(\mu'', v) = (l, \mu')}{\mu, \sigma, \&e_r \Downarrow (\mathbf{Ok} \ l, \mu')} $$

$$ \frac{\text{REFF} \qquad \mu, \sigma, e_r \Downarrow (\mathbf{Exc}, \mu')}{\mu, \sigma, \&e_r \Downarrow (\mathbf{Exc}, \mu')} $$

$$ \frac{\text{GET} \qquad \mu, \sigma, e_g \Downarrow (\mathbf{Ok} \ l, \mu') \qquad \mu'(l) = v}{\mu, \sigma, !e_g \Downarrow (\mathbf{Ok} \ v, \mu')} $$

$$ \frac{\text{GETF} \qquad \mu, \sigma, e_g \Downarrow (\mathbf{Exc}, \mu')}{\mu, \sigma, !e_g \Downarrow (\mathbf{Exc}, \mu')} $$

$$ \frac{\text{SET} \qquad \mu, \sigma, e_l \Downarrow (\mathbf{Ok} \ l, \mu'') \qquad \mu'', \sigma, e_v \Downarrow (\mathbf{Ok} \ v, \mu''') \qquad \mu''(l, v) = \mu'}{\mu, \sigma, e_l := e_v \Downarrow (\mathbf{Ok} \ (), \mu')} $$

$$ \frac{\text{SETF1} \qquad \mu, \sigma, e_l \Downarrow (\mathbf{Exc}, \mu')}{\mu, \sigma, e_l := e_v \Downarrow (\mathbf{Exc}, \mu')} $$

$$ \frac{\text{SETF2} \qquad \mu, \sigma, e_l \Downarrow (\mathbf{Ok} \ l, \mu'') \qquad \mu'', \sigma, e_v \Downarrow (\mathbf{Exc}, \mu')}{\mu, \sigma, e_l := e_v \Downarrow (\mathbf{Exc}, \mu')} $$

```
val output := st<exc<value>>
val eval (s:env)(e:expr) : output =
    branch ...
    or      let Add (e1,e2) = e in
              let Nat n1 =@ eval s e1 in
              let Nat n2 =@ eval s e2 in
              let n = add(n1,n2) in ret (Nat n)
    or      let Ref er = e in
              let v =@ eval s er in
              newref(v)
    or      let Get eg = e in
              let Loc l =@ eval s eg in
              get(l)
    or      let Set (el,ev) = e in
              let Loc l =@ eval s el in
              let v =@ eval s ev in
              set(l,v)
end
```

<caption>Figure 3.10: PCF with References</caption>
```h
val alloc: value -> st<loc>
val m_r: loc -> st<value>
val m_w: (loc, value) -> st<()>
val newref (v:value) : output =
  let l =@m alloc v in ret (Loc l)
val get (l:loc) : output =
  let r =@m m_r l in ret r
val set ((l,v):(loc,value)) : output =
  m_w(l,v);@m ret Unit
```

Note that the three concrete functions `alloc`, `m_r`, and `m_w` are left unspecified. In case of a failure of a memory reading via the `m_r` function, this function will fail in the skeletal semantics interpretation monad. Then, the following operators use these to encapsulate the result in the new PCF monad. The evaluation of the new constructors is straightforward. Note that the evaluation of pure terms (such as `Add`) does not need to be modified: defining the correct `bind` is sufficient to upgrade the semantics to the new monad.

If we compare to related frameworks—namely K [63], Ott [66], and Lem [55]—, there is no evidence that these languages can easily access the continuation of a program, hence introducing new features, such as the state, would mean cluttering the code with operations for handling them. Otherwise, if we consider the work of Wadler [72], we cannot reproduce the approach as Skel does support modules and functors. Nevertheless, the purpose of the languages we are writing is a substantial difference between the two works. Our approach shows how to write formalizations in a tiny framework, not interpreters in some complex meta-language such as OCaml or Haskell.

An affinity exists with the modular SOS [46], but we underline a substantial difference: we write machine code while modular SOS is a paper technique.
Instantiation

Again, to generate a working interpreter, after a run of `necroml`, one must only extend the `Types` functor with a definition to the location type, and the state, which is a map from locations to values. The state type is defined similarly to the environment, relying on the OCaml Map module type. Then, one needs to provide an implementation of the three concrete operations for manipulating the state concretely.

## 3.4 A Fully Monadic Skeletal Semantics

We now show how to extend the Skel definition in the previous section by introducing the reader monad to handle environment effects—the goal is to have a fully monadic Skel definition of the language of Section 3.3-. We will alter the evaluation function to consider the monadic environment operations. However, this approach makes a formalization more solid to further extensions. Indeed, this approach is convenient while writing large-scale formalizations, showing how one can gradually introduce under-the-hood behaviors in a semantic description by only adding or changing a few lines of code.

We want to make the environment manipulation happen implicitly.

First, we define the reader monad type and redefine the `bind` and the `exccont` binders. We show the `bind` code in the following snippet.

```haskell
type reader<a> := env -> a

val bind<a, b> (v:reader<st<exc<a>>>>>(f:(a -> reader<st<exc<b>>>>>)) :
    reader<st<exc<b>>>> =
    λs:env -> λm:state ->
        let (v', m') = v s m in
        branch let Exc = v' in let r = throw<b> () in r s m'
        or
        let Ok v'' = v' in f v'' s m'
    end
binder @ := bind
```
The reader monad, also called environment monad, serves to write programs in which all the operations may read data from an environment. In the bind shown above, we decided to combine the state, the exception, and the reader monad to obtain the following signature: `ENV → STATE → (EXC a, STATE)`, which in Skel is written as `reader<st<exc<a>>>`. Similarly to the bind, we write the `exccont`.

Then, as the reader monad is used to read an environment to provide data, we define a function ask on the computation of type `reader<st<exc<env>>>`. This function provides an environment to a program.

```haskell
val ask : reader<st<exc<env>>> = λs:env → λm:state -> ((Ok<env> s), m)
```

We can provide, to the continuations, manipulations of the environment via the usual local function. We write this function's signature similarly to the bind's and the `exccont`'s ones.

```haskell
val local<a> (s:reader<st<exc<env>>>) (f: () → reader<st<exc<a>>>):
    reader<st<exc<a>>> =
    λs_prev:env →
    λm:state → let (Ok s_new,m') = s s_prev m in
    f () s_new m'
```

Accordingly, we update the output alias type to be the one of the combination with the reader monad, and all the functions with the output sort of type `output`. Figure 3.11 shows the four monadic operations: `return` that returns a value in the `output` type, `newref` for a new allocation in the state, and `envGet` and `envExt`, the equivalent of the `getEnv` and `extEnv` functions, but returning a computation.

One of the purposes of updating the semantics is to manipulate the environment implicitly. Hence, we also define two functions for producing closures, either “normal” closures (`makeClosure`) or recursive ones (`makeRecursiveClosure`), and a function to get the environment from a closure (`closureEnv`). We show these three functions in Figure 3.12.

Finally, we update the evaluation function semantics. Let's start from its signature, which now changes to `val eval (e:expr) : output`. The reader can notice that we do not explicitly mention the environment (see Figure 3.10 for the old signature). Then, regarding the body of the `eval` function, we update only the constructors code manip-
```h
    type output := reader<st<exc<value>>>
    val return<a> (v:a) : reader<st<exc<a>>> =
        _:env -> !m:state -> (Ok<a> v,m)

    val newref (v:value) : output =
        _:env ->
        !m:state -> let ls = alloc v in
                   let (l,m') = ls m in
                     (Ok<value> (Loc l),m')

    val envGet (x:var) : output =
        let s =@ ask in
        let v = getEnv s x in ret v

    type env_output := reader<st<exc<env>>>
    val envExt ((x,v):(var,value)) : env_output =
        let s =@ ask in
        let s' = extEnv s x v in
        return<env> s'
```

<caption>Figure 3.11: Sample of the updated functions</caption>

ulating the environment, which are the variable term evaluation, the λ-term definition, the application, the let-in construct, and the fixed-point operator.

Let us start with the variable assignment `Var`. The semantics shown in Figure 3.8 is using the `getEnv` function to get the mapping of a variable `x` to a value `v` in an environment `s`, if any. Then return the value as a computation by applying the `ret` function to `v`. With the reader monad, we can return the result directly by applying the monadic function `envGet` to `x`, returning a value encapsulated in the monadic type.

```h
let Var x = e in envGet x
```

Then, we modify the λ-term's `eval` semantics. Evaluating `λx.eb` means to create a closure for `x`, `eb`, `s`, where `s` is the current environment. As the environment is no more explicit, we must ask for it, and only then create the closure. We designed a function to deal with this before, `makeClosure`. The constructor evaluation simply results in the following snippet.
```hhs
val makeClosure ((x,b):(var,expr)) : output =
    let s =@ ask in
    ret (Clos (x,b,s))
val makeRecursiveClosure ((x,b,f):(var,expr,var)) : output =
    let s =@ ask in
    ret (ClosRec (x,b,s,f))
val closureEnv (v:value) : env_output =
    branch let Clos (_,_,s) = v in return<env> s
    or let ClosRec (_,_,s,_) = v in return<env> s
    or let Nat _ = v in throw<env>()
    or let Unit = v in throw<env>()
    or let Loc _ = v in throw<env>()
end
```

<caption>Figure 3.12: Functions for creating closures. The output is a computation in the monad.</caption>

```hhs
let Lam (x,eb) = e in makeClosure(x,eb)
```

Regarding the application `e1 e2`, in Figure 3.8, we first evaluated `e1` in the current environment `s`, then evaluated `e2` in `s` and extended the environment accordingly on the resulting closure whether `e1` is recursive or not. In the fully monadic semantics, we do the same, feeding the new current environment to the continuation via the local `local` monadic binder, and using `closureEnv` and `envExt` to “automate” respectively reading an environment from a closure and extending or updating it. We show the code below.
```pascal
let App (e1,e2) = e in
let cl =@ eval e1 in
let w =@ eval e2 in
branch let Clos (x,eb,_) = cl in
    closureEnv cl;%local
    envExt(x, w);%local
    eval eb
or
    let ClosRec (x,eb,_,f) = cl in
    closureEnv cl;%local
    envExt(x, w);%local
    envExt(f, cl);%local
    eval eb
end
```

For the let-in construct, in the PCF semantics, first, we evaluated the expression to a value `v` to be mapped to a variable name `x` in an environment `s`, then extended the environment `s` with the mapping `x → v`, calling it `s'`, and finally returned the evaluation of the continuation in `s'`. The new code results in the following listing, where the `eval` call does not have the environment parameter anymore, and the computation contains the new environment, resulting from the application `envExt (x, v)`, which is directly bound to the continuation `eval eb`.

```pascal
let LetIn (x,ex,ec) = e in
let v =@ eval ex in
envExt(x, v);%local
eval ec
```

Finally, similarly to what we did with the application case, modifying the fixed-point `eval` code means simply using the `makeRecursiveClosure`. We show this below.

```pascal
let Fix (f, x, ex) = e in
makeRecursiveClosure(x,ex,f)
```

The rest of the evaluation function stays the same to what depicted in Figure 3.8 and 3.10. Concretely, the code evaluating the addition stays the same, as the rest of
the operations. One has only to delete the environment parameter from the `eval` calls.

```haskell
let Add (e1,e2) = e in
let Nat n1 =@ eval e1 in
let Nat n2 =@ eval e2 in
let n = add(n1,n2) in ret (Nat n)
```

Introducing a posteriori the reader monad needed some effort to define some new monadic helper functions and rewrite the parts of the semantics involving the environment. Nevertheless, the semantics presented will not change in the next section, showing that the approach is highly maintainable. The only change in writing the language extension of the next section is how we will deal with the monads, as we introduce one more new effect. The two language semantics presented in Section 3.3 are behaviourally equivalent. We did not prove this property formally.

### Instantiation

Introducing the reader monad in the semantic definition does not impact the instantiation of the interpreter. Indeed, we did not introduce any other new unspecified type or term. Hence, a user must only run `necroml` again and then use the same instantiation file of the stateful PCF.

## 3.5 Explicit Contination Manipulation

This section presents our most involved example by adding *delimited computations* to the language, following [31]. This complex transfer of control flow lets one start a computation, and this computation can suspend itself (*yield*) to return control to the calling computation, which can later resume the suspended computation. We combine this extension with exceptions and stateful computations. To this end, we use a *continuation monad* described in Section 3.5.2. To present the expected semantics, we describe it in the form of an abstract machine. Before these technical details, we give an intuition of the desired semantics through a series of examples in pseudo-code. The concept presented in the section finds a concrete use-case as future additions to OCaml [67].
1. `let x = {yield 1; yield 2; 3} in`
2. `handle x [`
3.   `ret v1: v1,`
4.   `cont v1 k1: let y = resume k1 in`
5.   `handle y [`
6.     `ret v2: v2,`
7.   `cont v2 k2: let z = resume k2 in`
8.   `handle z [`
9.     `ret v3: (100*v1 + 10*v2 + v3),`
10.   `cont v3 _: v3`
11. ]]]

<caption>Figure 3.13: Delimited Sequence of Yield</caption>

In the latter, the authors define language constructs for handling non-local control flow by manipulating stacked continuations.

### 3.5.1 Program Examples

Our first example is described in Figure 3.13. In Line 1, we assign the evaluation of the delimited computation `{yield 1; yield 2; 3}` to `x` (delimited computations are enclosed by curly braces). In this evaluation, `yield 1` suspends the computation and it returns both the value `1` and the continuation `{yield 2; 3}`. An *output* is thus a finished computation (with an actual value), or a suspension (with a value and a continuation). The `handle` operator takes such an output and two expressions, one to be executed if the computation is finished (field `ret`), and one if it is suspended (field `cont`). This can be seen in line 2 to 4. As `x` holds a suspension, the `cont` field is selected. It binds the value `1` to `v1` and the continuation to `k1`. This continuation is then resumed with the `resume` operator. Control is now passed to the continuation `k1` which corresponds to the code `{yield 2; 3}`. Evaluating this returns once again a suspended computation with value `2` and continuation `{3}`, which is bound to `y`. This suspended computation is handled one line 5, and the code on line 7 is then called. The continuation is once again resumed, and this time the delimited computation terminates with value `3`. Handling this output is done on line 8, and as it is finished, the `ret` case is selected. The expression `(100*v1 + 10*v2 + v3)` is then computed, returning 123.

An intuitive way to consider such computations is to imagine them as a stack, where
1 `let x ={let y = 1 in let z = yield y in (100*y + 10*z + yield 0)} in`
2 `handle x [`
3 `ret v1: v1,`
4 `cont v1 k1: let y = resume (k1, (v1 + 1)) in`
5 `handle y [`
6 `ret v2: v2,`
7 `cont v2 k2: let z = resume (k2, 3) in`
8 `handle z [`
9 `ret v3: v3;`
10 `cont v3 _: v3`
11 `]]]`

<caption>Figure 3.14: Two Ways Communication through Yield</caption>

the top of the stack is currently being executed. Creating a delimited computation `{e}`
adds it to the stack and evaluates it. Since `e` may itself start a delimited computation,
the stack can be arbitrarily tall. Once a computation returns, either suspended because
of `yield` or finished, the next computation in the stack starts evaluating. If the stack is
empty, then the program ends.

This example shows that the delimited section may communicate values to its con-
text (the next computation in the stack) using `yield`. We can make this communication
bidirectional by also passing a value when resuming a continuation. We show it in Fig-
ure 3.14. Now each time we resume a continuation, we send back a resumption value.
Indeed, the first `yield` in the example returns the value 1, which is the value the vari-
able `y` is bound to, and the rest of the delimited computation as continuation. When we
resume, in line 4, we resume the continuation `k1`, with a resumption value (`v1 + 1`),
with `v1` bound to 1. The expression `let z = yield y in` on line 1 creates the binding
`[z → 2]`. The delimited section suspends again at the evaluation of `yield 0`. Line 7 re-
sumes the computation communicating back the value 3. Finally, the delimited section
finishes computing returning to the handler the value 123, returned as final value of the
program.

3.5.2 Syntax and Semantics

To formally capture this semantics, we need to explicitly manipulate stacks of continu-
ations. We thus extend the syntax of the language presented in Section 3.4.
Formal Syntax

COUT o : ST(EXC(VAL))
CONT(α) κ : α → CSTACK(α) → α
CSTACK(α) π ::= ϵ | κα :: πα
VALUE v ::= ... | (v, κo) | κo
CONTM(α) ρ : CONT(α) → CSTACK(α) → α
EXPR e ::= ... | {e} | yield e | handle eh [ret xvr : er, cont xvc xk : ec]
| resume(ek, ev)

...  
type out := st<exc<value>>  
type cont<a> := a → cstack<a> → a  
type cstack<a> = | Nil | Cons (cont<a>, cstack<a>)  
type value = | ... | Susp (value, cont<out>) | Cont cont<out>  
type contM<a> := cont<a> → cstack<a> → a  
type expr = | ... | Run expr | Yield expr  
| Handle (expr, (var,expr), (var, var,expr))  
| Resume (expr, expr)

CONTM(α) is the monadic type constructor for the continuation monad. Given ρ of type CONTM(α), κ of type CONT(α) and π of type CSTACK(α), ρ κ π produces a value of type α, the result type of the program.

The CONT(α) type represents continuations: it is a function that expects a value and a stack of continuations to return a value. The type CSTACK(α) represents a stack of continuations. The stack may be empty, denoted with ϵ, or containing a continuation and the rest of the stack, represented as κ ::= π.

We extend also the VALUE type with suspension depicted as a tuple (v, κ), with
a value v and a continuation κ. We also add to values continuation themselves. For
instance, the evaluation of the sequence (yield e1; e2) returns a suspension value
(v1, k2), where v1 is the result of evaluating e1, and k2 corresponds to the suspended
evaluation of e2.

$$ \langle x, \kappa, \pi, \mu, \sigma \rangle_e \to [\kappa, \pi, \mu, \sigma, \text{Ok } v]_c \quad \text{with } v = \sigma(x) \qquad (3.1) $$

$$ \langle e_1 + e_2, \kappa, \pi, \mu, \sigma \rangle_e \to \langle e_1, (\Box + e_2) :: \kappa, \pi, \mu, \sigma \rangle_e \qquad (3.2) $$

$$ \langle n, \kappa, \pi, \mu, \sigma \rangle_e \to [\kappa, \pi, \mu, \sigma, \text{Ok } n]_c \qquad (3.3) $$

$$ [(\Box + e_2) :: \kappa, \pi, \mu, \sigma, \text{Ok } n_1]_c \to \langle e_2, (n_1 + \Box) :: \kappa, \pi, \mu, \sigma \rangle_e \qquad (3.4) $$

$$ [(n_1 + \Box) :: \kappa, \pi, \mu, \sigma, \text{Ok } n_2]_c \to [\kappa, \pi, \mu, \sigma, \text{Ok } n]_c \quad \text{with } n = n_1 + \mathbb{Z} n_2 \qquad (3.5) $$

$$ [f :: \kappa, \pi, \mu, \sigma, \text{Exc}]_c \to [\kappa, \pi, \mu, \sigma, \text{Exc}]_c \quad \forall e_2, f \neq \text{try}\{\Box\}\{e_2\} \qquad (3.6) $$

$$ [\text{try}\{\Box\}\{e_2\} :: \kappa, \pi, \mu, \sigma, \text{Exc}]_c \to \langle e_2, \kappa, \pi, \mu, \sigma \rangle_e \qquad (3.7) $$

$$ [\text{try}\{\Box\}\{e_2\} :: \kappa, \pi, \mu, \sigma, \text{Ok } v]_c \to [\kappa, \pi, \mu, \sigma, \text{Ok } v]_c \qquad (3.8) $$

$$ \langle e_{cl}e_v, \kappa, \pi, \mu, \sigma \rangle_e \to \langle e_{cl}, \Box e_v :: \kappa, \pi, \mu, \sigma \rangle_e \qquad (3.9) $$

$$ [\Box e_v :: \kappa, \pi, \mu, \sigma, \text{Ok } (x, e_x, \sigma_{cl})]_c \to \langle e_v, (x, e_x, \sigma_{cl}) \Box :: \kappa, \pi, \mu, \sigma \rangle_e \qquad (3.10) $$

$$ [(x, e_x, \sigma_{cl})\Box :: \kappa, \pi, \mu, \sigma, \text{Ok } v]_c \to \langle e_x, \kappa, \pi, \mu, (\sigma_{cl} + x \to v) \rangle_e \qquad (3.11) $$

$$ [\Box e_v :: \kappa, \pi, \mu, \sigma, \text{Ok } (x, e_x, \sigma_{cl}, f)]_c \to \langle e_v, (x, e_x, \sigma_{cl}, f) \Box :: \kappa, \pi, \mu, \sigma \rangle_e \qquad (3.12) $$

$$ [(x, e_x, \sigma_{cl}, f)\Box :: \kappa, \pi, \mu, \sigma, \text{Ok } v]_c \to \langle e_x, \kappa, \pi, \mu, (\sigma_{cl} + ((x \to v) + (f \to (x, e_x, \sigma_{cl}, f)))) \rangle_e \qquad (3.13) $$

$$ \langle e_l := e_v, \kappa, \pi, \mu, \sigma \rangle_e \to \langle e_l, \Box := e_v :: \kappa, \pi, \mu, \sigma \rangle_e \qquad (3.14) $$

$$ [\Box := e_v :: \kappa, \pi, \mu, \sigma, \text{Ok } l]_c \to \langle e_v, l := \Box :: \kappa, \pi, \mu, \sigma \rangle_e \qquad (3.15) $$

$$ [l := \Box :: \kappa, \pi, \mu, \sigma, \text{Ok } v]_c \to [\kappa, \pi, \mu', \sigma, \text{Ok } ()]_c \quad \mu(l, v) = \mu' \qquad (3.16) $$

$$ \langle \{e\}, \kappa, \pi, \mu, \sigma \rangle_e \to \langle e, \text{id}, \kappa :: \pi, \mu, \sigma \rangle_e \qquad (3.17) $$

$$ [\text{id}, \kappa :: \pi, \mu, \sigma, r]_c \to [\kappa, \pi, \mu, \sigma, r]_c \qquad (3.18) $$

$$ \langle \text{yield } e, \kappa, \pi, \mu, \sigma \rangle_e \to \langle e, \text{yield} \Box :: \kappa, \pi, \mu, \sigma \rangle_e \qquad (3.19) $$

$$ [\text{yield} \Box :: \kappa, \kappa' :: \pi, \mu, \sigma, \text{Ok } v]_c \to [\kappa', \pi, \mu, \sigma, \text{Ok } (v, \kappa)]_c \qquad (3.20) $$

$$ \langle \text{handle } e_h \quad [\text{ret } x_{vr} : e_r, \text{cont } x_{vc} : x_k : e_c], \kappa, \pi, \mu, \sigma \rangle_e \to \langle e_h, \text{handle} \Box \quad [\text{ret } x_{vr} : e_r, \text{cont } x_{vc} : x_k : e_c] \quad :: \kappa, \pi, \mu, \sigma \rangle_e \qquad (3.21) $$

$$ [\text{handle} \Box \quad [\text{ret } x_{vr} : e_r, \text{cont } x_{vc} : x_k : e_c] \quad :: \kappa, \pi, \mu, \sigma, \text{Ok } v]_c \to \langle e_r, \text{handle } v :: \kappa, \pi, \mu, (\sigma + x_{vr} \to v) \rangle_e \quad v \text{ pure} \qquad (3.22) $$

$$ [\text{handle} \Box \quad [\text{ret } x_{vr} : e_r, \text{cont } x_{vc} : x_k : e_c] \quad :: \kappa, \pi, \mu, \sigma, \text{Ok } (v, k)]_c \to \langle e_c, \text{handle } v :: \kappa, \pi, \mu, (\sigma + x_{vc} \to v + x_k \to k) \rangle_e \qquad (3.23) $$

$$ \langle \text{resume}(e_k, e_v), \kappa, \pi, \mu, \sigma \rangle_e \to \langle e_k, \text{resume}(\Box, e_v) :: \kappa, \pi, \mu, \sigma \rangle_e \qquad (3.24) $$

$$ [\text{resume}(\Box, e_v) :: \kappa, \pi, \mu, \sigma, \text{Ok } \kappa']_c \to \langle e_v, \text{resume}(\kappa', \Box) :: \kappa, \pi, \mu, \sigma \rangle_e \qquad (3.25) $$

$$ [\text{resume}(\kappa', \Box) :: \kappa, \pi, \mu, \sigma, \text{Ok } v]_c \to [\kappa', \kappa :: \pi, \mu, \sigma, \text{Ok } v]_c \qquad (3.26) $$

<caption>Figure 3.15: Abstract Machine for PCF + state + delimited continuations.</caption>
We extend the expressions with the following language constructors:

• `yield e`, for suspending a computation while returning the evaluation of `e`;

• `{e}`, for starting a delimited computation;

• `handle eh[ret xvr: er, cont xvc xk: ec]`, to inspect the result of the evaluation of `e`, distinguishing between a normal return or a suspension;

• `resume (ek, ev)`, where `ek` evaluates to a continuation, to resume it with the continuation value computed from `ev`.

To give a formal definition of our language, we need to switch paradigms, introduce in Section 1.3, as big step semantics are not convenient to describe suspended computations. To this end, one typically uses context-based reduction semantics or abstract machines. We choose the latter as the continuations are made explicit in that model. Our abstract machine is defined in Figure 3.15, with some similar rules omitted.

The abstract machine may be in one of two modes, one for evaluating expressions, and one for applying continuations. The evaluation mode, written as $\langle e, \kappa, \pi, \mu, \sigma \rangle_e$, evaluates `e` with a continuation $\kappa$, a continuation stack $\pi$, a state $\mu$ and an environment $\sigma$. Similarly, the continuation mode, denoted by $[\kappa, \pi, \mu, \sigma, r]_c$ applies the continuation $\kappa$ to the computed result $r$. A result is either an exception `Exc` or a normal result `Ok v`, where $v$ is either a pure value as before or a suspension $(v, \kappa)$.

A continuation is a stack of frames $f$ that contain an expression with a hole. For instance, when computing the first argument of an addition $t_1 + t_2$, the frame is $\Box + t_2$ (rule 3.2). When evaluating a constant, the machine switches to continuation mode (rule 3.3). Applying the frame $\Box + t_2$ to a value $n_1$ switches back to evaluation mode for $t_2$ with frame $n_1 + \Box$ (rule 3.4). Finally, applying this frame to a value $n_2$ computes $n_1 + n_2$ and passes it to the next frame by staying in continuation mode (rule 3.5).

Rules 3.6 to 3.8 show how exceptions are handled: if an exception is raised, it is caught by the first try frame. Otherwise, applying a try frame to a value simply passes control to the rest of the continuation.

Rules 3.9 to 3.13 deal with function and recursive function application. Rules 3.14 to 3.16 show how the heap may be mutated.

We now turn to two programs that involve delimited computations: `{1+2} + 3` and `{(yield 1)+2}`. The initial configuration of the abstract state machine for the first program is $\langle \{1+2\} + 3, \text{id}, \epsilon, \mu, \sigma \rangle_e$, where `id` represents the empty continuation. Applying
rule 3.2 results in $\langle\{1 + 2\}, (\Box + 3) :: id, \epsilon, \mu, \sigma\rangle_e$. Next, the machine uses rule 3.17 to enter the delimited computation. It push the current continuation on the continuation stack and starts evaluation $1+2$ with a new empty continuation, resulting in the configuration $\langle 1+2, id, ((\Box + 3) :: id) :: \epsilon, \mu, \sigma\rangle_e$. The addition is then evaluated as above, before reaching configuration $[id, ((\Box + 3) :: id) :: \epsilon, \mu, \sigma, Ok 3]_c$. The delimited computation is finished as only the empty continuation remains, so the previous continuation is restored with the computed value (rule 3.18): $[(\Box + 3), id, \epsilon, \mu, \sigma, Ok 3]_c$. The computation then proceeds to the final state $[id, \epsilon, \mu, \sigma, Ok 6]_c$.

The second program starts with configuration $\langle\{(yield 1)+2\}, id, \epsilon, \mu, \sigma\rangle_e$. The derivation proceeds in a similar way as the previous example till we reach the `yield` with a configuration $\langle yield 1, (\Box+2) :: id, id :: \epsilon, \mu, \sigma\rangle_e$. Now by applying rule 3.19, we first evaluate the constant expression 1 in the configuration $\langle 1, yield \Box :: (\Box+2) :: id, id :: \epsilon, \mu, \sigma\rangle_e$. Hence, we end up in the continuation configuration $[yield \Box :: (\Box+2) :: id, id :: \epsilon, \mu, \sigma, Ok 1]_c$. Rule 3.20 restores the continuation at the top of the stack as current continuation (here `id`), and a suspension as result: $[id, \epsilon, \mu, \sigma, Ok (1, (\Box+2) :: id)]_c$. As the suspension is not resumed, the computation ends here and the addition is not performed.

We next turn to two examples using the `handle` construct.

```
(* A *)
handle ({1 + 2} + 3) [
  ret v1: v1,
  cont _ _: skip
]
```

```
(* B *)
handle {yield 1 + 2} [
  ret v1: v1,
  cont v1 k1: let x = resume (k1,v1 + 3) in
    handle x [
      ret v2: v2,
      cont v2 _: v2 ]]
```

Consider the following as initial configuration for listing A.

$\langle \text{handle} (\{1 + 2\} + 3) [\text{ret } v1:v1, \text{cont } v1 \ _:v1], \text{id}, \epsilon, \mu, \sigma \rangle_e$

By applying rule 3.21, the expression $\{1 + 2\} + 3$ is first evaluated, resulting in a continuation configuration of the form:

$[\text{handle} \Box [\text{ret } v1:v1, \text{cont } _ _:\text{skip}] :: id, \epsilon, \mu, \sigma, Ok 6]_c$. This time the evaluation is not yet complete, as the current continuation holds the remainder of the `handle` construct. The value in the continuation configuration is 6, a pure value, so the next
thing to do is to evaluate the expression in the `ret` field of the handler. By rule 3.22, this result in $\langle v1, \text{id}, \epsilon, \mu, (\sigma + v1 \rightarrow 6) \rangle_e$. The next step accesses the environment— rule 3.1-to lead to a final configuration $[\text{id}, \epsilon, \mu, \sigma, \text{Ok } 6]_c$.

We now turn to listing B. After evaluating the `yield` construct, we reach the following configuration.

$[\text{handle } \square \quad [\text{ret } v1:v1, \text{cont } v1 \quad k1:\dots]] :: \text{id}, \epsilon, \mu, \sigma, \text{Ok} \quad (1, (\square + 2) :: \text{id})]_c$

The evaluation of the expression `{yield 1 + 2}` returns a suspension which is a pair with a value 1 and the reminder of the delimited section computation $(\square + 2) :: \text{id}$. As the suspension is not a pure value, the evaluation proceeds by applying rule 3.23 on the latter configuration. We obtain the following, where $\sigma'$ is $\sigma + (v1 \rightarrow 1) + (k1 \rightarrow (\square + 2) :: \text{id})$.

$\langle \text{let } x = \text{resume}(k1, v1 + 3) \text{ in } \dots, \text{id}, \epsilon, \mu, \sigma' \rangle_e$

We first apply the evaluation rule for `let` (not shown), yielding this configuration.

$\langle \text{resume}(k1, v1 + 3), (\text{let } x = \square \text{ in } \dots) :: \text{id}, \epsilon, \mu, \sigma' \rangle_e$

We apply rule 3.24 to start the evaluation of `k1`, then rule 3.25 to start the evaluation of `v1 + 3`. We then reach the following configuration, the first square of the `resume` is part of the stored continuation `k1`, whereas the second square is waiting for the resumption value.

$[\text{resume}((\square + 2) :: \text{id}, \square) :: (\text{let } x = \square \text{ in } \dots) :: \text{id}, \epsilon, \mu, \sigma', \text{Ok } 4]_c$

Resuming a continuation means evaluating in, passing to it the last value computed. The current continuation $((\text{let } x = \square \text{ in } \dots) :: \text{id})$ is itself stored at the top of the stack. After applying rule 3.26, we obtain the following configuration.

$[(\square + 2) :: \text{id}, ((\text{let } x = \square \text{ in } \dots) :: \text{id}) :: \epsilon, \mu, \sigma, \text{Ok } 4]_c$

After evaluating the addition and applying rule 3.18 for the identity continuation, we
```pascal
type output := reader<contM<st<exc<value>>>>
  val eval (e:expr) : output =
    branch ...
  or      let Add (e1,e2) = e in
                 let Nat n1 =@ eval e1 in
                 let Nat n2 =@ eval e2 in
                 let n = add(n1,n2) in ret (Nat n)
  or      let Run e' = e in ();%pushCont
                 eval e'
  or      let Yield e' = e in
                 let v =@ eval e' in susp v
  or      let Handle (eh,(xvr,er),(xvc,xk,ec)) = e in
                 let v =@ eval eh in
                 branch let v = getPure v in
                             envExt(xvr, v);%local eval er
                 or      let (v,k) = getSusp v in
                             envExt(xvc, v);%local envExt(xk, (Cont k));%local
                             eval ec
                       end
  or      let Resume (ek,ev) = e in
                 let kv =@ eval ek in
                 let v =@ eval ev in
                 let k = getCont kv in resume k v
end
```

<caption>Figure 3.16: Yield Language in Skel</caption>

obtain the following configuration.

$$ [let x = \square \ in \ handle x \ [ret v2: v2, cont v2 _: v2], id, \epsilon, \mu, \sigma, Ok 6]_c$$

The rest of the derivations follows the pattern of the first handle example, leading to a final configuration $[id, \epsilon, \mu, \sigma, Ok 6]_c$.

### 3.5.3 A Stateful PCF Language with Yield and Exceptions in Skel

We now present the Skel formalization of the language described in Section 3.5.2. As before, we change the meaning of monadic binders and returns, to keep the main
description of the semantics unchanged.

Our semantics is described in Figure 3.16. We highlight the addition rule, showing it is not modified. As before, the behavioral complexity of dealing with continuations for previously existing constructs is delegated to the monadic binders `binder @ := bind` and `binder ? := exccont`.

The `bind` function works as follows. It expects a computation `w` in the monad `reader<contM<st<exc<a>>>>>`, a function `f` to apply after the computation, and it should return a term in the same monad. To do so, we first request (using `λ` abstractions) the environment `s`, the continuation `k` to apply after `w` and `f`, the current continuation stack `ks`, and the current state `m`. We then execute `w` with a new continuation, detailed below, the stack `ks`, and the state `m`. The intuition behind the new continuation is that it should proceed with `f` if the result is not an exception, passing `k` to it as continuation, otherwise it should return the exception using `k`. The new continuation is defined as follows. It first take a computation `vse` in the state and exception monad, the current stack `ks1`, and the current state `m1`. It then applies `vse` to `m1` to obtain an exception value `ve` and a new state `m2`. The exception value is then inspected. If it is an exception, it is passed (embedded in the state monad) to the continuation `k` with stack `ks1` and updated state `s2`. Otherwise, it is a value `v` which we pass to `f`, with the environment `s`, continuation `k`, stack `ks1`, and state `m2`.

The behavior of `extcont` is similar, reversing the two inner branches. Note that we could simplify the code for the binders by removing some eta-expansions for state `m` and stack `ks`, we keep them for clarity. We show the code of the `bind` function below.
```h
val bind<a> (w:reader<contM<st<exc<a>>>>>)
           (f:a -> reader<contM<st<exc<a>>>>>) :
            reader<contM<st<exc<a>>>>> =
            λs:env ->
            λk:cont<st<exc<a>>>> ->
            λks:cstack<st<exc<a>>>> ->
            λm:state -> w s (λvse:st<exc<a>>>>
                             λks1: cstack<st<exc<a>>>> ->
                             λm1:state ->
                             let (ve,m2) = vse m1 in
                             branch let Exc = ve in
                             k (λm3:state -> (Exc<a>,m3)) ks1 m2
                             or
                             let Ok v = ve in
                             let w' = f v in w' s k ks1 m2
                             end) ks m
```

The rule for a new delimited computation `{e}` is defined in the `Run` branch. It pushes the current continuation on the continuation stack and runs `e` using the identity continuation (Similar to rule 3.17). To simplify the code, we use the monadic binder `pushCont` to push the continuation. We show the code below.

```h
val id (v:out)(ks:cstack<out>):out =
  λm:state ->
    branch let Nil = ks in v m
    or
    let Cons (k, ks') = ks in k v ks' m
end
```

```h
val pushCont (_:()) (f:()→output):output =
  λ_:_env -> λk:cont<out> -> λks:cstack<out> ->
    f () id (Cons<out>(k,ks))
```

This snippet also contains the code for the identity continuation, which returns the final value if the stack is empty, otherwise it passes this value to the next continuation on the stack, as in rule 3.18 of Figure 3.15.
The `Yield` rule is straightforward with our monad. We first evaluate its argument expression to `v`, then we call `susp` to suspend the current computation `k`. This function extracts the continuation `k'` at the top of the stack and calls it with the value `Susp(v, k)`. We present its definition in the following listing.

```haskell
val susp (v:value):output =
  λ_ : env ->
  λk : cont<out> ->
  λks : cstack<out> ->
  let Cons (k', ks') = ks in
  k' (λs:state → (Ok<value> (Susp (v,k)), s)) ks'
```

The `Handle` construct defines two cases, depending on the result of the evaluation of `eh`. In the pure case `v`, the environment `s` is extended with a binding `xvr → v` and we evaluate `er`. This case corresponds to the abstract machine rule 3.22. In the suspension case `(v,k)`, the environment is extended by `xvc → v` and `xk → k`, then `er` is evaluated. This follows rule 3.23.

Finally, `Resume(ek, ev)` is the constructor for resuming a suspended computation. We first evaluate `ek` to a continuation `k` (rule 3.24) and `ev` to a value `v` (rule 3.25). Then, the `resume k v` call performs the behavior of rule 3.26. Basically, it puts `k` as current computation to evaluate, and pushes the actual current continuation on top of the stack. The continuation `k` is resumed with the value `v` and the new stack. We show the code below.

```haskell
val resume (kv:cont<out>)(v:value):output =
  λ_ : env ->
  λk : cont<out> ->
  λks : cstack<out> ->
  kv (λm:state → (Ok<value> v, m))
  (Cons<out> (k, ks))
```

In Figure 3.17, we show a final example of program. In this example, we interleave state updates in a delimited computation and in the calling code. This program shows that the state is global. Communication between delimited code is bidirectional, both in an explicit way, through suspensions and resumption values, and in an implicit way
1 let x = { let y = &1 in
2         let x1 = !y in
3         let x2 = !(yield y) in
4         yield(y := 1);
5         (100*x1 + 10*x2 + (!y)) } in
6 handle x [
7     ret v1: v1,
8     cont r k1:
9         r := 2;
10        handle (resume (k1,r)) [
11            ret v2: v2,
12            cont _ k2:
13                r := !r + 2;
14            handle (resume (k2,r)) [
15                ret v3: v3,
16                cont v3 _: v3]]]

<caption>Figure 3.17: Ping-Pong State Updates through Yield</caption>

through state updates. The result of the program is again 123.

Instantiation

Once the user generate via `necroml` the file `.ml`, it can just use
the same instantiation file defined for the stateful PCF (Sec-
tion 3.3).

3.6 Related Work

There are many criteria to evaluate the formalization of a programming language: it should be easy to write and to reuse, it should be close to the specification if there is one, it should be executable to be tested, and it should be usable, for instance to prove properties of programs or the language itself, or to mechanically manipulate the semantics. In this Chapter, we do not directly address the last two points, but we remark that skeletal semantics can be translated to OCaml interpreters using [42], and to Coq formalizations using [50]. Recent work uses this approach to derive a certified
interpreter [1].

The formalization of a language may take several forms: it can be given as an interpreter, it can be defined in a proof assistant, or it can be described in a framework providing a meta-language and tools to manipulate the formalization.

An interpreter may be considered to be a formalization of a language if it is written in a clear way and if the host language has itself a clear semantics. Consider for instance engine262 [22]: the code is very close to the specification of JavaScript, but the host language is JavaScript itself, which is quite complex. In fact, engine262 uses JavaScript's generators to formalise them,<fnref n="2" /> hence it does not clarify how they work. Implementations as specifications can be useful to give an intuition of the semantics of a language, but they do not provide a simple way to manipulate the semantics or to prove properties.

Many languages have been directly formalised in Coq [70], such as C in the setting of CompCert [39] or JavaScript [6], while others have been formalised in Isabelle/HOL [29], such as ML in the setting of CakeML [37]. Using extraction mechanisms, some of these semantics can be made executable. These works are impressive achievements, but they suffer from two shortcomings. First, replicating them for a new language requires a significant effort. Second, the semantics defined cannot be easily manipulated, for instance to mechanically transform them.

To alleviate these issues, one may use a framework in which the language is described, and from which implementations or formal definitions in proof assistants may be derived. These generated implementations may not be as elegant as when done by hand, but they can be easily adapted when needed, for instance switching from a big-step semantics to a small-step one, or going from a shallow embedding to a deep embedding. This is the approach followed by skeletal semantics, as well as many other frameworks such as Ott [66], Lem [55], and K [63]. The distinguishing feature of skeletal semantics is how simple the meta-language is: it does not come with any predefined semantics nor does it try to deal with complex syntactic features such as binders. The cost of this choice is that a skeletal semantics description of a language may require more work—complexity of the approach relies in monadic function definitions-, but the benefits is that skeletal semantics can be easily extended in the language itself, through the use of monads as illustrated in this Chapter. This is because skeletal pro-

<footnote n="2">2. https://github.com/engine262/engine262/blob/206928332324f0ae95485aee9784dbf19e525b36/src/abstract-ops/generator-operations.mjs#L245</footnote>
grams are almost in Administrative Normal Form [64], thus removing the need to use a
CPS transformation to have access to continuations [24]. It is not clear how one would
add delimited computations to the previously cited frameworks. Another benefit, pre-
sented in Chapter 2, is the existence of a simple API to manipulate skeletal semantics,
enabling the creation of many tools based on the same input language.
<figure><img src="image_21.png" /></figure>
# A FAITHFUL DESCRIPTION OF ECMASCRIPT IN SKELETAL SEMANTICS

## Contents

<table><tr><td>4.1</td><td>ECMAScript Algorithms in Skel</td><td>87</td></tr><tr><td>4.1.1</td><td>ECMAScript</td><td>87</td></tr><tr><td>4.1.2</td><td>Challenges of the Formalization</td><td>88</td></tr><tr><td>4.1.3</td><td>Completion Record and the ECMAScript Error Handling (?)</td><td>97</td></tr><tr><td>4.1.4</td><td>A Control-Flow monad</td><td>100</td></tr><tr><td>4.1.5</td><td>A Real Example in Skel</td><td>103</td></tr><tr><td>4.1.6</td><td>Current Status</td><td>106</td></tr><tr><td>4.2</td><td>Interpreter Evaluation</td><td>109</td></tr><tr><td>4.2.1</td><td>Interpreter Instantiation</td><td>109</td></tr><tr><td>4.2.2</td><td>Evaluation</td><td>110</td></tr><tr><td>4.3</td><td>Related Work</td><td>113</td></tr></table>

« Ora et labora »

- Saint Benedict

## Introduction

This chapter shows that the Skeletal Semantics framework [8, 54] is suitable for mechanizing a real-world specification. To this end, we describe the ongoing formalization
of ECMAScript—formal semantics of JavaScript-algorithms in Skel. Differently from
Chapter 3, the document presenting the language defines the evaluation as algorithms,
allowing us to show that our approach is suitable also to mechanize this type of defini-
tion. We show that the resulting description is very close to the specification. In addition,
we have formalized enough algorithms to be able to run simple JavaScript programs
and thus test our approach.

The project is the first formalization of a real-world programming language in Skel, the meta-language used to write Skeletal Semantics. This work strongly supported the evolution of Skel, from the introduction of the notion of polymorphism to the addition of monads and first-class functions. This evolution is motivated by the need to have a formal semantics and a language expressive enough to capture the behavior of ECMAScript algorithms, ensuring a visual and a behavioral match between the formalization and the specification.

Our main effort is presenting the description of the mechanization of a core EC-
MAScript algorithm in Section 4.1, where we also present some crucial features of
Skeletal Semantics, which significantly improve the readability of the mechanization,
inspired by the approach presented in Chapter 3. In Section 4.2, we evaluate our ap-
proach, and finally, in Section 4.3, we discuss previous work on JS semantics.

Contribution

In this chapter we present:

* the design of a concise, readable, maintainable and textu-
  ally close writing approach to model complex algorithmic
  specifications in Skel, namely ECMAScript.

* an ongoing formalization of ECMAScript in Skel.

* an instantiation of a JavaScript interpreter generated from
  a semantic framework.

* some executions of small JavaScript programs.

<footnote>The contributions of this chapter are part of a national [34] and an inter-
national(PPDP’22) [33] publication.</footnote>
# 4.1 ECMAScript Algorithms in Skel

In this section, we illustrate how we formalize ECMAScript(ES) algorithms in Skel. In Section 4.1.1, we provide some context about the ES specification. Then, in Sections 4.1.2, 4.1.3, and 4.1.4, we introduce methods to use the tiny Skel language for handling and combining ECMAScript's side-effects, ending up in a structured and systematic way for describing the algorithms. In Section 4.1.5, we present the formalization of the *GetValue<fnref n="1" /> Internal Method* as representative of our approach. The *GetValue* method is one of the most referenced in ES, and is also enough complex to describe our systematic approach to formalizing of ES algorithms. Finally, in Section 4.1.6, we detail the current state of the work.

## 4.1.1 ECMAScript

ECMAScript is a large vernacular specification written in an imperative style. It is divided into 28 chapters and six appendices. Despite its complexity and verbosity, it provides a complete specification of the behavior of JS. However, some choices are left to the implementation, so a formalization must consider these unspecified pieces. We will explain later how we deal with them.

After an introductive part in chapters 1 to 5, where the notational and algorithmic conventions are defined, the document can be divided into three main functional groups.

Chapters 6, 7, and 9 give a taxonomy of ES *Data Types and Values*, providing each taxon with a definition of its operations and related invariant, followed by the definition of *abstract operations* (type conversion, comparison, object, and iterator operations), the *runtime environment*, and detailed classification of the type *Object* and its internal methods. This block of chapters gives a complete overview of the execution environment in which an ES program should be executed. Formalizing any language construct first requires a formalization of this execution environment.

Chapter 8 defines some syntax-directed operations. The central part of the specification, chapter 10 to chapter 16, describes the actual ES programming language. Chapters 10 and 11 focus on lexical units. Language constructs are given in chapters 12 to 15, where each construct is given with its syntactic specification and its eval-

<footnote n="1">1. https://tc39.es/ecma262/2021/#sec-getvalue</footnote>
uation. These describe expressions, statements, functions, and scripts. Modules are
defined in chapter 16.

Chapters 17 to 27 introduce the default components of the *Global Object*. In addition, a memory model is given in Chapter 28.

4.1.2 Challenges of the Formalization

The first step of the mechanization in the purely functional Skel language is to deal with
the imperative nature of the specification, raising two issues.

First, there is a notion of an implementation-dependent state that can be mutated.
More precisely, we define by *state* the aggregation of all the imperative data manipu-
lated by the specification. We design it as a record that includes the Execution Context
stack, a strictness boolean flag, and a pool of Maps holding *Execution Contexts*, *Envi-
ronment Records*, *Realms*, *Script Records*, and *Objects*. In the Skel artefact, we have
fully defined both the state and its helper functions. To remain close to the imperative
specification, we design a Skel state monad in Figure 4.1. This monad lets us implicitly
pass the state around, similarly to what we showed in Section 3.3. Note that we could
have left these “implementation-dependent” elements of the specification unspecified,
providing an implementation to this type and its function after generating an artefact.

Second, the specification often breaks the usual control flow by having a *return* in the middle of algorithms. We can capture such control flows by using nested branches (see below), but this significantly reduces the legibility of the mechanization. We thus define a *control flow* monad to simplify the mechanization. In addition, the specification itself introduces operators that behave much like an exception monad to deal with *break*, *function returns*, or *exceptions*.

We thus propose in Section 4.1.3 an exception monad that captures the behavior of
ES monadic shorthands ? and !,<fnref n="2" /> and in Section 4.1.4, its extension to handle control-
flow features. We claim the combination of the state monad with the control-flow and
the exception ones dramatically simplifies our code, making the Skel description of ES
algorithms easy to write and maintain. The result is close to the specification, as shown
in Section 4.1.5.

<footnote n="2">2. https://tc39.es/ecma262/2021/#sec-returnifabrupt-shorthands</footnote>
type state (* specified in the artefact *)

type st<a> := state → (a, state)

val st_bind<a,b> (v:st<a>) (f:(a → st<b>)): st<b> =
  λs: state →
  let (v', s') = v s in f v' s'
val st_ret<a>: (v: a) : st<a> = λs: state → (v, s)

<caption>Figure 4.1: State Monad in Skel</caption>

## Example of Implementation Dependent Choices: The State

The state is fully defined in the artefact, represented as a Skel record with eight fields. In the following paragraphs, we present a broad explanation of how we implemented data stored in the state. Most of the elements in the ES memory are left “implementation dependent”, which gives much space for misinterpretation or different correct implementations. We tried to study the manuscript to describe these structures by retrieving information from the ES document.

### Execution Contexts

An execution context is an ES specification data structure used to keep track of the runtime evaluation of executable code by an ES implementation. In the document, there is a broad description of what concretely is this specification device. We quote its definition.

### ECMAScript

> An execution context contains whatever implementation specific state is necessary to track the execution progress of its associated code.

This definition is complemented with a table providing a broad definition of how one can implement it. Indeed the table defines four fields:

*   **Code evaluation state:** "Any state needed to perform, suspend, and resume evaluation of the code associated with this execution context".

*   **Function:** "If this execution context is evaluating the code of a function object, then the value of this component is that function object. If the context is evaluating the code of a Script or Module, the value is null."
* **Realm**: "The Realm Record from which associated code accesses ECMAScript resources."

* **ScriptOrModule**: "The Module Record or Script Record from which associated code originates. If there is no originating script or module, as is the case for the original execution context created in InitializeHostDefinedRealm, the value is null."

Accordingly to the definition in the table, in Skel, we define a record defining eight fields, one for each bullet of the previous list plus three extra fields not defined in the table but accessed and modified by some algorithmic steps in the document.

```typescript
type executionContext = (
  _CodeEvaluationState: codeEvaluationState,
  _EC_Function: maybeNull<locObject>,
  _Realm: option<loc_realmRecord>,
  _ScriptOrModule: maybeNull<scriptOrModule>,
  _VariableEnvironment: option<loc_EnvironmentRecord>,
  _LexicalEnvironment: option<loc_EnvironmentRecord>,
  _Generator: maybeNull<locObject>
)
```

The type `maybeNull` is an option value similar to the classic `maybe` type in Haskell or the `option` type in OCaml. The difference is that, in this case, the options for `maybeNull` are between being `MNNull`, referring to the ECMAScript value `null`, or being the polymorphic constructor `MNNotNull` of type `a`, to say that the value is not `null`. Throughout the formalization, we define types similar to this to create an option between an ECMAScript pure value and different kinds of data. Another option is to reify by defining a sum type containing all the types in the formalization. This choice has been ignored as it is complicated to give a precise number of the types in the ES document as it is untyped. The type `executionContext` is extended with three extra fields retrieved while reading and writing the formalization. Making choices happens quite often as the internal data structures are broadly defined, being "implementation dependent". We reference the execution contexts in the Skel implementation. This structure is stored in a mapping in the state itself, relating locations to execution contexts.
**Execution Context Stack** In the specification, the execution context stack is defined textually as:

### ECMAScript

The execution context stack is used to track execution contexts. The running execution context is always the top element of this stack. A new execution context is created whenever control is transferred from the executable code associated with the currently running execution context to executable code that is not associated with that execution context. The newly created execution context is pushed onto the stack and becomes the running execution context.

In Skel, we do not have any implementation of this data structure, so we chose to represent the type stack as an unspecified type. We also define the type helper functions to manipulate the stack. The execution contexts held in the stack have a status field. In case of an execution context suspension, some algorithmic steps of the specification may be suspended too. In this case, before resuming, the latter suspended execution context resumes the suspended code, possibly altering the state, and then evaluates the algorithmic steps following its resumption. This mechanism is quite complex and, in the context of the thesis, causes problems in handling the execution context stack, as continuations manipulate the normal LIFO behavior of the stack data structure. Indeed, in the following text, we present sentences of the specification which hint at the more complex control flow of the algorithmic steps.

### ECMAScript

Evaluation of code by the running execution context may be suspended at various points defined within this specification. Once the running execution context has been suspended a different execution context may become the running execution context and commence evaluating its code. At some later time a suspended execution context may again become the running execution context and continue evaluating its code at the point where it had previously been suspended. Transition of the running execution context status among execution contexts usually occurs in stack-like last-in/first-out manner. However, some ECMAScript features require non-LIFO transitions of the running execution context.

We plan to change the actual formalization, including the work shown in Section 3.5.
An execution context can be seen as a delimited code section, which can yield, pro-
ducing a non-linear behavior of the executable specification code. In Section 4.1.6, we
will describe how these non-LIFO manipulations of the execution context stack can in-
validate some of our ES formalization features, such as a simple function call with at
least one argument.

**Environment Records** The Environment Record is a specification type used to define the association of Identifiers to specific variables and functions based upon the lexical nesting structure of ECMAScript code. Usually, an Environment Record is associated with some specific syntactic structure of ECMAScript code, such as a *FunctionDeclaration*, a *BlockStatement*, or a *Catch* clause of a *TryStatement*. Each time such code is evaluated, a new Environment Record is created to record the identifier bindings created by that code.

This record, merely a specification mechanism, cannot be accessed and modified
by programs, as it is considered internal to an interpreter. The specification does not
provide directions on how to implement this data structure as it is unnecessary, giving
free will in describing it. As the project's goal is a loyal formalization of the specifica-
tion, we tried to collect every possible information about the execution contexts in the
document to provide a reference implementation. We must say that the specification
provides a classification of this record.

This record can be a *Declarative Record*, used to define the effect of ECMAScript
language syntactic elements such as FunctionDeclarations, VariableDeclarations, and
Catch clauses that directly associate identifier bindings with ECMAScript language val-
ues (Null, Undefined, Boolean, Number,BigInt, String, Symbol, and Object). A Declara-
tive Record can be a *Function Environment Record*, storing information about bindings
for the top-level declarations within that function and establishing a new *this* binding.
Also, it captures the state necessary to support super method invocations, or a *Module
Environment Record*, containing the bindings for the top-level declarations of a mod-
ule. This work focused more on the semantics of evaluating the scripts rather than JS
modular code and modules. Hence, we did not represent the latter category. Then, the
record can be an *Object Environment Record* or a *Global Environment Record*. For
the first category, the record defines the effects of some ECMAScript elements that
associate identifier bindings with the properties of some object.
An example can be the relation between Object Environment Records and the With-
**Statement.** This Environment Record type associated with a *with* statement can provide its bound object as an implicit argument of a function call. This argument is the *this* value of the called function.

The second record type is used for the script's global declarations. It may be prepop-
ulated with identifier bindings and includes an associated global object, the standard
library of JavaScript.

The Environment Records have a field called [[OuterEnv]], a mechanism that en-
ables the hoisting feature—default behavior of moving all declarations to the top of
the current scope. This mechanism is similar to accessing properties via the proto-
type chain, a link between objects that establishes a hierarchy between objects and
prototypes that define them.

The record we design is a record containing all the fields of all the possible cat-
egories of environment records. Then, we can identify the type of a given environ-
ment record by defining an extra field providing the type. We decided not to rely on
the typical duck-typing<fnref n="3" /> of languages such as JavaScript, which is not convenient be-
cause of Skel being a strongly typed language. Non-mandatory fields are defined as
option-type fields, according to our understanding of the specification. The record is
too big to be reported in this thesis. It can be inspected at the following URL: https:
//gitlab.inria.fr/skeletons/jskel/-/blob/matches/semantics/js.sk#L4479.

We also provide getter and setter functions that manipulate the mapping between
locations (numbers) and environment records in the state. In the Skel implementation,
we always reference the environment records, resolving the mapping only if we need
to manipulate the referenced record's contents.

In the record, we define a field for each one of the internal methods. These are
higher-order fields. An instance of the Environment Record has each function instanti-
ated with its location, allowing one to apply the method by only passing the arguments
defined in the specification. For example, given an environment record er, if we want to
call its internal method _Method_ with parameter par, we do er._Method_ par. Implicit
in the call is the location of the record er.

**Realm Records** This record consists of a set of intrinsic objects, an ECMAScript global environment, all of the ECMAScript code executing within the scope of that global environment, and some other associated resources.

<footnote n="3">3. "If it walks like a duck, and it quacks like a duck, then it must be a duck."</footnote>
The intrinsic objects are the standard library of the language. They are the prototype of all the possible features that a custom-defined object might have. We design the intrinsic object field as a record in which each field is labeled after the specification name of each intrinsic object (%ObjectName%) and has the object's location as its value. Then, the record contains a reference to the environment of the global object, the first environment created while instantiating program interpretation. The ECMAScript code field has the AST of the program currently being evaluated. Then there are additional pieces of information, such as the [[TemplateMap]], which we do not currently consider, and the [[HostDefined]] field, providing some additional features to the language, extending what the standard defined. For example, NodeJS implements the server language extension as host-defined features. These custom features are more related to implementations of the language rather than the standard itself. We do not consider this field in our formalization.

In the implementation, we map locations to Realm Records, as with the other records stored in the state. Then the state field is a map. Realm Record does not have internal methods, but it is often manipulated. For that, we design a set of accessors and modifiers to manipulate the actual Realm Record stored in the state.

**Script Records** The Script Record is a specification mechanism containing information about the evaluation of a script. It is implemented similarly to the other records. It references the Realm Record in which the script is evaluated, the environment in which the top-level bindings of the script are stored, the ES AST representing the program, and some host-defined additional information related to the script evaluation. Its implementation goes straightforwardly with the one of the Environment Record.

**Objects** ECMAScript objects are not fundamentally class-based such as those in C++, Smalltalk, or Java. Instead, objects may be created in various ways, including via a literal notation or via constructors. These create objects and execute code that initializes all or part of them by assigning initial values to their properties. Each constructor is a function that has a property named "prototype", which is used to implement prototype-based inheritance and shared properties.

Like the Environment Records, also the objects are categorized. We implement the object type as a record containing all the object types' fields and properties, turning on and off an object field via option-like type values. All the internal methods store the
object's location, providing uniformity to the overall formalization approach. We again do not rely on the duck-typing by adding an extra field describing the type of the instantiated object. In Figure 4.2, we present the object's internal representation `{n : 42}`. This output is produced after interpreting the program via the OCaml interpreter generated from Skel. The field `_ObjectType_` shows object type, an `OrdinaryObject`. The binding of the property `n` to `42` is the first element of the property list—field `_Properties_`. Each internal method of the object is instantiated with a `this` value, a reference to the object itself.

We handle the objects stored in the state as we did with the previous records, making the state field `_Objects_` a mapping between locations and the actual type encoding objects.

In the artefact, we provide a complete description of all the categories of objects. We do not list them here, as presenting them does not provide additional information on the approach to formalizing the ES document. Nevertheless, the type definition is available at https://gitlab.inria.fr/skeletons/jskel/-/blob/matches/semantics/js.sk#L1714.

**A Local Environment** The local environment is not defined in the document but is necessary for our approach. The specification style is pseudo-algorithmic. It often happens that a new name not existing in the upper scope of an algorithmic step is created inside an inner scope and then propagated to the top-level contexts. The specification implicitly defines a hoisting method in the context of single ES steps. We add to the state a local environment to hoist these bindings outside the scope of an algorithmic step. In Figure 4.3, we provide an example of these algorithmic steps. In the first step, a new name `bar` is set to false if `foo` is true. In the second step, the bar is inspected, but in the case of `foo` being `false`, generally, the specification considers the `bar` value `undefined`. We use the local environment first to set all the inner-scope instantiated names as undefined. Then we manipulate these names in this special context, outside the skeletal semantics' one.