I am currently:
- a PhD student since October 2020 under the suvervision of Catherine Dubois (Samovar, ENSIIE), and Valentin Blot (LMF, Université Paris-Saclay),
- a member of Deducteam (an Inria Saclay team) of the LMF laboratory,
- funded by the Labex Digicosme.
Research
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.
Teaching
- 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.
Talk
- LMF seminar on K
- LVP Research Day
- TransForm working group
- Deducteam working group on Metamath
- CEA list seminar: Soon
Publication
- Co-authored with Mathieu Montin and Catherine Dubois. LIBNDT: Towards a formal library on spreadable properties over linked nested datatypes - MSFP 2022.
Not yet available. - Co-authored with Valentin Blot and Catherine Dubois. Vers une traduction de K en Dedukti - JFLA 2022.
Not yet available. - Co-authored with Catherine Dubois. FaCiLe en Coq : vérification formelle des listes d'intervalles - JFLA 2020.
Available here.
Contact
For research purpose, please contact me at: amelie (dot) ledein (at) inria (dot) fr
