< Retour au sommaire

Vers une traduction de K en Dedukti

Amélie Ledein le

Lieu: Amphithéâtres 33/34

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, nous présentons un outil de traduction de K vers Dedukti, appelé KaMeLo. 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.