Amélie Ledein

Je suis actuellement :

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

  • 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
  • Journée de recherche LVP
  • Groupe de travail TransForm
  • Groupe de travail Deducteam sur Metamath
  • Séminaire CEA list : Bientôt

Publication

Contact

Pour toutes questions relatives à mes travaux de recherche, merci de me contacter à l'adresse :
amelie (dot) ledein (at) inria (dot) fr