Yoan Geran

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.
  • Draft : A Canonical Form For Universe Levels in Impredicative Type Theory

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
  • 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.