Je suis actuellement :
- en thèse depuis le 1er octobre 2020 sous la supervision de Catherine Dubois (Samovar, ENSIIE), et de Valentin Blot (LMF, Université Paris-Saclay),
- membre de Deducteam (une équipe de Inria Saclay) du laboratoire LMF,
- financée par le Labex Digicosme.
Recherche
Mots-clefs : Interopérabilité, Assistant de preuve, Sémantique, Réécriture, Théorie des types.
Outils : Coq, Dedukti, K, Agda, Metamath.
Je m'intéresse à la vérification de preuves de sémantique formelle (comme par exemple la preuve qu’un langage est déterministe ou la propriété dite de subject reduction) de langages de programmation ainsi que la réutilisation de ces preuves dans un autre assistant à la preuve.
J'étudie plus particulièrement le framework K, un framework permettant de définir des sémantiques formelles de langages de programmation à partir desquelles différents outils sont automatiquement dérivés, ainsi que Dedukti, un framework logique permettant l'interopérabilité des preuves entre différents outils de preuve formelle.
D'un point de vue logique, K est basé sur la Matching Logic tandis que Dedukti est basé sur le LambdaPi-calcul modulo théorie.
Mes objectifs principaux sont plus particulièrement :
- Traduire une sémantique K en Dedukti.
- Traduire un programme écrit dans un langage décrit par une sémantique K, en Dedukti.
- Encoder la Matching Logic dans le LambdaPi-calcul modulo théorie.
- Vérifier des preuves K en Dedukti.
- Permettre l'interopérabilité des sémantiques grâce à Dedukti.
- Permettre le multi-formalisme des sémantiques.
Enseignement
- 2022/2023 - ENS Paris-Saclay
- Programmation fonctionnelle (Compilateur Go écrit en OCaml (projet), L3, 15h) avec Yoan Géran, Louis Lemonnier, Mihaela Sighireanu et Thomas Chatain.
- Génie logiciel (Projet, M1, 27h) avec Thomas Chatain.
- Projet Logique (Tutoriel et projet en Coq, L3, 22h30).
- 2021/2022 - ENS Paris-Saclay
- Programmation fonctionnelle (Compilateur Go écrit en OCaml (projet), L3, 15h) avec Louis Lemonnier, Mihaela Sighireanu et Thomas Chatain.
- Logique (TD, L3, 15h) avec Luc Chabassier.
- Projet Logique (Tutoriel et projet en Coq, L3, 22h30).
- 2020/2021 - ENS Paris-Saclay
- Programmation fonctionnelle (TD + Compilateur C écrit en OCaml (projet), L3, 30h) avec Gabriel Hondet, Mihaela Sighireanu et Jean Goubault.
- Programmation orientée-objet (Projet en Scala, L3, 15h) avec Stefan Schwoon et Mathieu Hilaire.
- Génie logiciel (Projet, M1, 30h) avec David Baelde.
Présentation
- Séminaire LMF sur K - 23 mars 2021
- Journée de recherche LVP - 23 novembre 2021
- Groupe de travail TransForm - 7 décembre 2021
- Groupe de travail Deducteam sur Metamath - 6 janvier 2022
- Séminaire CEA list - 31 mars 2022
Publication
- Co-écrit avec Mathieu Montin et Catherine Dubois. LIBNDT: Towards a formal library on spreadable properties over linked nested datatypes - MSFP 2022.
Pas encore disponible. - Co-écrit avec Valentin Blot et Catherine Dubois. Vers une traduction de K en Dedukti - JFLA 2022.
Pas encore disponible. - Co-écrit avec Catherine Dubois. FaCiLe en Coq : vérification formelle des listes d'intervalles - JFLA 2020.
Disponible ici.
Contact
Pour toutes questions relatives à mes travaux de recherche, merci de me contacter à l'adresse :
amelie (dot) ledein (at) inria (dot) fr
