Members

Co-founders

• Davide Barbarossa — Università di Bologna
  Lambda-calculus, type theory, linear logic, category theory, classical realizability, philosophy of mathematics
• Pablo Donato 🌸 — Grothendieck Institute administrator
  Proof theory, type theory, topos theory, proof assistants, human-computer interaction, end-user programming
• Boris Eng 🦖 — R&D engineer at OCamlPro administratorcoordinator
  Transcendental syntax, proof theory, linear logic
• Valentin Maestracci — Université Aix-Marseille
  Lambda-calculus, type theory, homotopy type theory, Dedukti, directed homotopy theory, rewriting

Members

• Victor Benitah — Airline pilot at Air France
  Formal systems explorer, co-founder of an electronic firm
• Hugo Cadière — Université Jean-Moulin Lyon 3
  Philosophy of mathematics / computer science / language / mind, German Idealism and XXth century German philosophy
• Pierre Cardascia 🎲 — SubOptimal Games
  Philosophy, Game Design, Entrepreneurship, Immersive Experience, Poetry
• Baptiste Chanus — Université Paris 1 Panthéon-Sorbonne
  Descriptive complexity
• Kostia Chardonnet — Centre Inria de l'Université de Lorraine (MOCQUA)
  Computer science, quantum computation, cyclic proofs
• Sidney Congard — Centre Inria de l'Université de Rennes (Gallinette)
  Semantics of programming languages
• Xavier Denis
  Deductive verification and specification of Rust programs
• Pierre Benjamin Giraud — Centre Inria de l'Université de Rennes (Gallinette)
  Multi-dimensional (Logic x Cubes & Rewriting systems x Automata), automata for proofs, philoTechny of mathematics
• Charles Grellois — University of Sheffield
  Semantics, (linear) logic, automata theory, higher-order model-checking, mathematical modeling, probabilistic termination
• Jérémy Hervé 🍄 — Independent external communications
  Mushrooms, operating systems design
• Ambroise Lafont — École Polytechnique (LIX)
  Type Theory and Category Theory
• Luc Pommeret — LISN Paris-Saclay
  Logic, LLM (Machine learning)
• Adrien Ragot — Université Sorbonne Paris Nord / University Roma Tre
  Proof-nets, interaction nets, implicit computational complexity, lambda-calculus, linear logic
• Paul Séjourné — Université Paris-Sorbonne
  Archaic and contemporary philosophy (of mathematics), algebraic geometry, category theory
• Vincent Moreau — Université Paris Cité (IRIF)
  Category theory, type theory, denotational semantics, topology, algebra, proof assistants
• François-René Rideau (Faré)
• Tito — CNRS & Aix-Marseille
  Links between linear logic and automata theory, combinatorics, computational complexity, algorithms

Visitors and guests

Titouan Carette, Clémence Chanavat, Bernardo Marques, Julien Marquet, Rémi Nollet, Federico Olimpieri, Raphaël Tossings, Pierre Vial, Quentin, Gaël Deest, Martin Tricaud, Fadi Shawki, Éliès Harington, Axel Kerinec, Aloÿs Dufour, Bernardo, Anne-Laure, Escherichia, Alexey, Roman Perez, Nico, Chirine Laghjichi, Jonty Male, Alexis Toumi, Baptiste Colin, Léo, Noé Ensarguet.