- I am a PhD student since October 2021 under the supervision of Olivier Hermant and Gilles Dowek.
- I am a member of CRI, and of the LMF, in the Deducteam team.
Research
I am interested in type theory, proof assistant, rewriting, and proof systems interoperability. I study the expression of Coq in the LambdaPi-calculus modulo theory, and more particularly the expression of the universe polymorphism together with an impredicative universe Prop. This aims interoperability through the logical framework Dedukti.
My main objectives are the following.
- Translation of Calculus of Constructions with universe polymorphism into Dedukti.
- Translation of Coq into Dedukti.
- Simplification of proofs (reverse mathematics).
- Use Dedukti to share proofs in first-order logic into tactic languages of proof assistants.
Teaching
- 2023/2024 - ENS Paris-Saclay
- Programming, exercise sessions (C and ASM, L3)
- Project, functionnal programming (C compiler and memory allocator in OCaml, L3).
- Project, object-oriented programming (Simulation game in Scala, L3).
- 2022/2023 - ENS Paris-Saclay
- Project, functionnal programming (Go compiler in OCaml, L3).
- Project, object-oriented programming (Strategy game in Scala, L3).
- Networks, exercise sessions (M1)
- 2021/2022
- Programming and algorithms, exercise sessions, ENSTA Paris (C, L3)
- Programming and algorithms, exercise sessions, IUT Orsay (C++, L1)
For research or teaching purposes, don't hesitate to contact me at yoan.geran (at) minesparis (dot) psl (dot) eu.