Thursday 24 March 2022, 3:00 PM, room 3U47 and online: Vers une traduction de K en Dedukti, Amélie Ledein (Deducteam, INRIA, LMF, Université Paris-Saclay).

K est un framework sémantique permettant de décrire formellement des sémantiques de langages de programmation. C'est aussi un environnement qui offre différents outils pour aider à la programmation avec les langages spécifiés dans le formalisme. Il est par exemple possible d'exécuter des programmes et de vérifier certaines propriétés sur ceux-ci, à l'aide de l'outil KProver. K repose sur une logique du 1er ordre munie d'une application entre formules et d'opérateurs de point fixe, d'égalité, de typage ainsi que d'un opérateur similaire à l'opérateur “next” des logiques temporelles. Ce dernier opérateur permet d'encoder la sémantique des programmes par la réécriture.

Dedukti est un framework logique permettant l'interopérabilité des preuves entre différents outils de preuve formelle. Il possède des plugins d'import et d'export pour des systèmes de preuve aussi divers que Coq, PVS ou encore Isabelle/HOL. Il repose sur le LambdaPi-calcul modulo théorie, une extension de la théorie des types par l'ajout de règles de réécriture dans la relation de conversion. La flexibilité de ce framework logique permet d'encoder de nombreuses théories comme la logique du 1er ordre ou la théorie des types simples.

Dans le cadre de ce séminaire, qui a pour objectif la présentation de mes travaux de thèse, je présenterai mon outil de traduction de K vers Dedukti, appelé KaMeLo, qui, à ce stade, permet l'exécution de sémantiques K en Dedukti. Cet outil a pour objectif, à plus long terme, de permettre la vérification des preuves faites au sein de K et la réutilisation de sémantiques formelles de langages de programmation ainsi que des propriétés sur leurs programmes au sein de nombreux systèmes de preuve, via Dedukti.