---
title: "Members"
---

# Co-founders

- [Davide Barbarossa](https://davidebarbarossa12.github.io/index.html)<div class="desc-box">Lambda-calculus, type theory, linear logic, category theory, classical realizability, philosophy of mathematics --  Università di Bologna</div>
- [Pablo Donato 🌸](http://www.lix.polytechnique.fr/Labo/Pablo.DONATO/) (administrator)<div class="desc-box">Sequent calculus, deep inference, type theory, Peirce's existential graphs, focalization, proof search -- Ecole Polytechnique</a>
- [Boris Eng 🦖](https://www.engboris.fr) (administrator)<div class="desc-box">Computer science, transcendental syntax -- OCamlPro / SuperBOL</a>
- Valentin Maestracci<div class="desc-box">Lambda-calculus, type theory, homotopy type theory, Dedukti, directed homotopy theory, rewriting -- Université Aix-Marseille</a>

# Members 

- Baptiste Chanus<div class="desc-box">Descriptive complexity -- Université Paris 1 Panthéon-Sorbonne</div>
- [Kostia Chardonnet](https://kostiachardonnet.github.io/)<div class="desc-box">Computer science, quantum computation, cyclic proofs -- Centre Inria de l'Université de Lorraine (MOCQUA)</div>
- [Sidney Congard](https://dwarfobserver.github.io/)<div class="desc-box">Semantics of programming languages -- Centre Inria de l'Université de Rennes (Galinette)</div>
- Jérémy Hervé 🍄<div class="desc-box">Mushrooms -- Independent</div>
- [Ambroise Lafont](https://amblafont.github.io/)<div class="desc-box">Type Theory and Category Theory -- University of Cambridge</div>
- Luc Pommeret
- Adrien Ragot<div class="desc-box">Proof-nets, interaction nets, implicit computational complexity, lambda-calculus, linear logic -- Université Sorbonne Paris Nord / University Roma Tre</div>
- Paul Séjourné<div class="desc-box">Philosophy (Aristotle, Kant, Deleuze), algebraic geometry, category theory -- Université Paris-Sorbonne</div>
- Vincent Moreau<div class="desc-box">Category theory, type theory, denotational semantics, topology, algebra, proof assistants -- Université Paris Cité (IRIF)</div>
- [Tito](https://nguyentito.eu/)<div class="desc-box">Links between linear logic and automata theory, combinatorics, computational complexity, algorithms -- École normale supérieure de Lyon</div>
- [Xavier Denis](https://xav.io/)<div class="desc-box">Deductive verification and specification of Rust programs -- ETH Zurich</div>

# Visitors and guests

Hugo Cadière, Titouan Carette, Clémence Chanavat, Bernardo Marques, Julien Marquet, Rémi Nollet, Federico Olimpieri, Raphael Tossings, Pierre Vial, Quentin, Gael Deest, Martin Tricaud, Fadi Shawki, Eliès Harington, Axel Kerinec, Aloÿs Dufour, Bernardo, Anne-Laure, Escherichia, Alexey.