Université de Rennes 1 Skeletal semantics transformations Transformations de sémantiques squelettiques Sémantiques squelettiquesSémantiques opérationnellesGrand-pasPetit-pasMachines abstraitesInterprétation certifiée Skeletal semanticsOperational semanticsBig-stepSmall-Stepabstract MachinesCertified Interpretation Sémantique opérationnelle 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é. Skeletal semantics is a framework to describe the operational semantics of programming languages. We first present an automatic translation of a skeletal semantics written in big-step style into an equivalent structural operational semantics. This translation is implemented on top of the Necro tool, which lets us automatically generate an OCaml interpreter for the small-step semantics and a Coq mechanization of both semantics. We prove the transformation correct in two ways: we provide a paper proof of the core of the translation, and we generate Coq certification scripts alongside the transformation. We also propose an automatic generation of a certified OCaml interpreter for any language written in skeletal semantics. To this end, we introduce two new interpretations, i.e., formal meanings, of skeletal semantics, in the form of non-deterministic and deterministic abstract machines. These machines are derived from the usual big-step interpretation of skeletal semantics using functional correspondence, a standard transformation from big-step evaluators to abstract machines. All these interpretations are formalized in the Coq proof assistant and we certify their soundness. We finally use the extraction from Coq to OCaml to obtain the certified interpreter. Electronic Thesis or DissertationText en application/pdf1 : 1324 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/a14fb0b5-2e47-4fa2-af7c-01461c0a3de8 Ambal Guillaume 1995-11-29 FR 26712533X guillaume+rennes@ambal.fr 2022REN1S057 http://www.theses.fr/2022REN1S057 2022-10-19 Informatique Universite de Rennes 1thesis.degree.grantor_1 02778715X Doctorat non ouiSchmittAlanintervenant_1135454840BertrandNathalieintervenant_2111647339MadiotJean-Marieintervenant_4184897262LengletSergueïintervenant_5142299847HirschkoffDanielintervenant_7123325382TassonChristineintervenant_3142544108Biernacki‎Diaruszintervenant_6267149468 MATHSTICecoleDoctorale_1 204770424 IRISA partenaireRecherche_1 026386909 ddc:004 SchmittAlanBertrandNathalieTassonChristineMadiotJean-MarieLengletSergueïBiernacki‎DiaruszHirschkoffDanielUniversite de Rennes 1Sciences et technologie, medecine, pharmacie, odontologie, droit, economie, gestion, philosophieMATHSTICÉcole doctorale Mathématiques et sciences et technologies de l'information et de la communication (Rennes) IRISA ASCII PDF 1355662