Titre de la soutenance : Sémantiques Squelettiques pour Calculs de Processus

Résumé :

Les sémantiques squelettiques sont un cadre logique pour décrire les sémantiques opérationnelles.
Tout d'abord, nous présentons une transformation automatique d'une sémantique squelettique écrite en style grand-pas vers une sémantique équivalente en style petit-pas. Cette transformation est implémentée dans l'outil Necro, ce qui nous permet de générer automatiquement un interpréteur OCaml pour la sémantique petit-pas ainsi qu'une formalisation Coq des deux sémantiques. Nous certifions la transformation de deux manières : nous donnons une preuve papier du cœur de la transformation, et nous générons des scripts de preuve Coq spécialisés durant la transformation.
Nous proposons également une méthode automatique pour générer un interpréteur OCaml certifié pour n'importe quel langage défini en sémantiques squelettiques. Pour cela, nous présentons deux nouvelles interprétations des sémantiques squelettiques, sous la forme de machines abstraites déterministe et non-déterministe. Ces machines sont obtenues à partir de l'interprétation grand-pas principale en utilisant la correspondance fonctionnelle, une méthode connue pour transformer un évaluateur en machine abstraite. Ces nouvelles interprétations sont formalisées en Coq, et nous vérifions leur correction.
Enfin, nous utilisons le système d'extraction de Coq vers OCaml pour obtenir un interpréteur certifié.