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

Defense type
Thesis
Starting date
End date
Location
IRISA Rennes
Room
Salle METIVIER - 10h00
Speaker
Adam KHAYAM - Equipe EPICURE
Theme
"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.

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

Composition of the jury
Rapporteurs:
- RYU Sukyoung, professeure, School of Computing, Korea Advanced Institute of Science and Technology
- DUBOIS Catherine, professeure, ENSIIE, Evry

Examinateurs : 
- RIVAL Xavier, directeur de recherche, INRIA Paris
- CHARGUÉRAUD Arthur, chargé de recherche, INRIA Nancy

Dir. de thèse : 
- SCHMITT Alan, directeur de recherche, INRIA Rennes 
- REZK Tamara, directrice de recherche, INRIA Sophia-Antipolis

- BLAZY Sandrine, professeure, Rennes 1