Amélie Ledein

I am currently:


Keywords : Interoperability, Proof assistant, Semantic, Rewriting, Type theory.

Tools : Coq, Dedukti, K, Agda, Metamath.

I am interested in the verification of formal semantic proofs (such as the proof that a language is deterministic or the so-called "subject reduction" property) of programming languages and the reuse of these proofs in another proof assistant.

I study more particularly the K framework, a framework allowing to define formal semantics of programming languages from which different tools are automatically derived, as well as Dedukti, a logical framework allowing the interoperability of proofs between different formal proof tools.

From a logical point of view, K is based on Matching Logic while Dedukti is based on LambdaPi-calculus modulo theory.

My main objectives are more specifically :

  • Translate a K semantics into Dedukti.
  • Translate a program written in a language described by a K semantics, into Dedukti.
  • Encoding Matching Logic in the LambdaPi-calculus modulo theory.
  • Verify K proofs in Dedukti.
  • Allow interoperability of semantics through Dedukti.
  • Allow multi-formalism of semantics.


  • 2021/2022 - ENS Paris-Saclay
    • Functional programming (Go compiler in OCaml (project), L3, 15h) with Louis Lemonnier, Mihaela Sighireanu and Thomas Chatain.
    • Logique (TD, L3, 15h) with Luc Chabassier.
    • Projet Logique (Tutorial and project in Coq, L3, 22h30).
  • 2020/2021 - ENS Paris-Saclay
    • Functional programming (TD + C compiler in OCaml (project), L3, 30h) with Gabriel Hondet, Mihaela Sighireanu and Jean Goubault.
    • Oriented-object programming (Project in Scala, L3, 15h) with Stefan Schwoon and Mathieu Hilaire.
    • Software Engineering (Project, M1, 30h) with David Baelde.


  • LMF seminar on K
  • LVP Research Day
  • TransForm working group
  • Deducteam working group on Metamath
  • CEA list seminar: Soon



For research purpose, please contact me at: amelie (dot) ledein (at) inria (dot) fr