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

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.

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."