Computer science & mathematics
I am mostly interested in programming languages, logic, category
theory and geometric insights on these subjects as can be given by
algebraic topology and algebraic geometry.
I am currently doing a post-doc at Gallinette, Inria Rennes with Nicolas Tabareau
and Éric Tanter around dependent types,
universes and effects (with gradual stuff interleaved).
Before that, I worked under the supervision of Cătălin Hriţcu
around the programming language F* (and
more precisely Dijkstra Monads - see publications for details or this
PhD manuscript) in the team
Prosecco, at Inria Paris and
also spent some time torturing robots at Mujin.
Publications & Pre-publications
- SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
C. Abate, P. G. Haselwarter, E. Rivas, A. Van Muylder, T. Winterhalter, C. Hriţcu and B. Spitters
Presented and published at CSF'21
The formal development is accessible on github
- Gradualizing the Calculus of Inductive Constructions
Meven Lennon-Bertrand, Nicolas Tabareau and Éric Tanter
(submitted for journal publication)
- Mettons de l'ordre dans CIC !
(presented at JFLA 21, in French)
A short abstract presenting a work in progress program to develop ordered syntactic models of the Calculus of Constructions.
The formal development corresponding to the note is available here.
- On relational verification for monadic programs
Cătălin Hriţcu, Exequiel Rivas and Antoine Van Muylder
Presented and published at POPL'20
- Dijkstra Monads for All
D. Ahman, R. Atkey, G. Martinez, C. Hriţcu, E. Rivas, É. Tanter
Presented and published at ICFP'19
- Recalling a Witness: monotonic state in F*
D. Ahman, C. Fournet, C. Hritcu, A. Rastogi, N. Swamy
Presented and published at POPL'18
- Monadic reification in F*
N. Grimm, C. Fournet, C. Hriţcu, M. Maffei, J. Protzenko, T. Ramananandro, A. Rastogi, N. Swamy, S. Zanella-Béguelin
Presented and published at CPP'18
- Dijkstra Monads for Free
D. Ahman, C. Hriţcu, G. Martinez, G. Plotkin, J. Protzenko, A. Rastogi, N. Swamy
Presented and published at POPL'17
- A Fibrational Account of Local States
Presented and published at LICS'15
Thèse de doctorat (PhD)
I prepared my PhD under the supervision of Cătălin Hriţcu at ENS Ulm and team Prosecco, Inria Paris on Principles of Program Verification For Arbitrary Monadic Effects.
I defended on November 25th, 2019 at Inria, Paris in front of a jury composed by
The slides of the presentation can be found here.
- President: Hugo Herbelin
- Reviewer: Shin-Ya Katsumata
- Reviewer: Bas Spitters
- Examiner: Robert Atkey
- Examiner: Gilles Barthe
- Examiner: Pierre-Évariste Dagand
- Examiner: Christine Paulin-Mohring
- Examiner: Nicolas Tabareau
- Advisor: Cătălin Hriţcu
- On the F* language (slides - GeoCal-Lac 17, ChoCoLa (Dec. 17), Eutypes 18)
- On μ̃μ (slides - at Gallium Seminar (Oct. 18) - small variation on Gabriel's HOPE'18 presentation)
- On Dijkstra monads (slides - GT Scalp 18, Prosecco Seminar (Dec. 18), Eutypes 19)
- On syntactic models of CIC (slides presented at LHC 21)
I really like cooking, in particular french and japanese cuisine !