Thibaut Benjamin
Welcome to my personal webpage
Introduction
I am a maître de conférences (associate professor) in computer science at LMF (laboratoire méthodes formelles), in Université Paris-Saclay. I work at the intersection of type theory and higher categories, exploring how they inform each other. I got my PhD from LIX, Ecole Polytechnique under the direction of Samuel Mimram and Eric Finster, and I have worked as a postdoc at the University of Cambridge in the team of Jamie Vicary, part of the CLASH research group. I also did a postdoc in the development team of Frama-C at CEA List where I worked with Julien Signoles on runtime verification of C programs.
Research Interests
My research interests lie in the intersection between computer science and mathematics. I am particularly interested in the semantics of these languages, and the connection it establishes between programming and reasonning via the Curry-Howard correspondence.
I am particularly interested in all the languages whose semantics can be cleanly defined, and enjoy rich algebraic properties, like the functional languages, as I find those encourage good practice and high maintainability. I also like that these languages interact well with proof-assistants (I particularly use Agda and Rocq).
I am also interested in higher category theory and homotopy theory, as a way to understand equality and rewriting, as started by the development of homotopy type theory.
Keywords:
- Programming language semantics
- Logic
- Category theory
- Dependent type theory
- Homotopy type theory
- Formal methods
- Proof-assistants
Other Scientific Interests
Beside my work as a computer scientist, I am interested in science in general as I like to feel my understanding of the world evolve. I also like science history, to witness how ideas grew to be at the point they currently are. I particularly value science communication and I admire the content creators that can give access to beautiful and important science results to non-specialist.
Free and open source software
I support free and open source software. My personal experience with it has been that paid alternatives are often worse, albeit sometimes easier to begin. I try to contribute to the projects that I use when I can.
Welcome to my personal webpage
Introduction
I am a maître de conférences (associate professor) in computer science at LMF (laboratoire méthodes formelles), in Université Paris-Saclay. I work at the intersection of type theory and higher categories, exploring how they inform each other. I got my PhD from LIX, Ecole Polytechnique under the direction of Samuel Mimram and Eric Finster, and I have worked as a postdoc at the University of Cambridge in the team of Jamie Vicary, part of the CLASH research group. I also did a postdoc in the development team of Frama-C at CEA List where I worked with Julien Signoles on runtime verification of C programs.
Research Interests
My research interests lie in the intersection between computer science and mathematics. I am particularly interested in the semantics of these languages, and the connection it establishes between programming and reasonning via the Curry-Howard correspondence.
I am particularly interested in all the languages whose semantics can be cleanly defined, and enjoy rich algebraic properties, like the functional languages, as I find those encourage good practice and high maintainability. I also like that these languages interact well with proof-assistants (I particularly use Agda and Rocq).
I am also interested in higher category theory and homotopy theory, as a way to understand equality and rewriting, as started by the development of homotopy type theory.
Keywords:
- Programming language semantics
- Logic
- Category theory
- Dependent type theory
- Homotopy type theory
- Formal methods
- Proof-assistants
Other Scientific Interests
Beside my work as a computer scientist, I am interested in science in general as I like to feel my understanding of the world evolve. I also like science history, to witness how ideas grew to be at the point they currently are. I particularly value science communication and I admire the content creators that can give access to beautiful and important science results to non-specialist.
Free and open source software
I support free and open source software. My personal experience with it has been that paid alternatives are often worse, albeit sometimes easier to begin. I try to contribute to the projects that I use when I can.