ReFL
Reflexions sur les Fondements de la Logique
2022 – 2026
What ReFL was
ReFL was a French scientific network on the foundations of logic and computation. It was founded by four PhD students during the "Linear Logic Winter School 2022", and grew into a broader community bringing together logicians, computer scientists, mathematicians and philosophers, from academia as well as from industry, who shared a taste for deep questions and the ambition of proposing original insights on the foundations of computation and logic. The role of computer science in understanding logic was a constant concern.
The group was inspired by the transdisciplinarity of the LIGC working group, which gathered researchers from various fields around the foundations of (linear) logic. Discussions, seminars and meetings were held in French, but English speakers were always welcome.
Its recurring interests were the foundations and philosophy of logic, computation and mathematics, the history of logic and computation, category theory and its applications, the proof-program correspondence and proof/type theory, and the works of Jean-Yves Girard: linear logic, proof-nets, ludics, geometry of interaction and transcendental syntax.
Its activities were online seminars, debates on Zulip, private in-person meetings, mutual assistance around theses, research and programming, and collective writing and programming projects.
Founders
- Davide Barbarossa Università di Bologna Lambda-calculus, type theory, linear logic, category theory, classical realizability, philosophy of mathematics
- Pablo Donato Charles University Proof theory, type theory, category theory, proof assistants, end-user programming
- Boris Eng OCamlPro Transcendental syntax, proof theory, linear logic
- Valentin Maestracci Université Aix-Marseille Lambda-calculus, type theory, homotopy type theory, Dedukti, directed homotopy theory, rewriting
Members
Over the years, ReFL also gathered:
- Victor Benitah Formal systems explorer, co-founder of an electronic firm
- Hugo Cadière Philosophy of mathematics / computer science / language / mind, German Idealism and XXth century German philosophy
- Pierre Cardascia Philosophy, game design, entrepreneurship, immersive experience, poetry
- Baptiste Chanus Descriptive complexity
- Sidney Congard Semantics of programming languages
- Xavier Denis Deductive verification and specification of Rust programs
- Pierre Benjamin Giraud Multi-dimensional (logic x cubes & rewriting systems x automata), automata for proofs, philoTechny of mathematics
- Charles Grellois Semantics, (linear) logic, automata theory, higher-order model-checking, mathematical modeling, probabilistic termination
- Jérémy Hervé Mushrooms, operating systems design
- Cécile Janin Embedded electronic systems, instrumentation, FPGA Linux
- Ambroise Lafont Type theory and category theory
- Eric Patrizio Frugality of programming languages, degrowth computing
- Roman Perez Philosophy of logic and language
- Luc Pommeret Logic, LLM (machine learning)
- Adrien Ragot Proof-nets, interaction nets, implicit computational complexity, lambda-calculus, linear logic
- François-René Rideau (Faré)
- Paul Séjourné Archaic and contemporary philosophy (of mathematics), algebraic geometry, category theory
One last gathering
Farewell meeting in Antony
October 10, 2026 · Organized by Pierre Benjamin Giraud
Before the community closes for good, a final meeting takes place in Antony. Details are given by email to past members.
Past events
Some meetings were private and informal. For these reasons, they are not recorded here.
-
Meeting ReFLi 2026 in Lizio, Morbihan
June 27 – July 1st, 2026 -
Artificial intelligence
Jan 22, 2026- Artificial intelligence and formal proofs Luc Pommeret · 40min
-
Meeting around Jean-Yves Girard
Nov 23, 2025 -
Meeting ReFLi 2025 in Lizio, Morbihan
April 28 – May 2, 2025 -
Fondements esthétiques de la logique
November 1, 2024- Morts du mythe, de l'art, de la philosophie, de la logique : Itinéraire d'un problème serial-killer Pierre Cardascia · 1h30
-
Introduction to transcendental syntax
June 20, 2024 -
Analytic and continental philosophy
May 20, 2024- Le professionnel et l'écrivain : le pouvoir offensif de la philosophie analytique Luc Pommeret · 1h30
-
Technical introduction to transcendental syntax
May 11, 2024- Introduction to Peirce's philosophy Pablo Donato · 30min
- Stellar resolution and Girard's knitting Boris Eng
-
Meeting around Jean-Yves Girard
May 10, 2024 -
Program verification
June 26, 2023- Presentation of the Rust programming language Xavier Denis · 1h
- Why formal verification is getting it wrong Xavier Denis · 1h
-
Logic and quantum computation
May 31, 2023- Quantum computation and Geometry of Interaction Kostia Chardonnet · 45min
-
Logic and Categories
March 24, 2023- Pourquoi les catégories sont la bonne façon de faire de la sémantique dénotationnelle Tito · 1h
- Catégories monoïdales à trace Valentin Maestracci · 1h
-
ReFL first seminar of the year
February 21, 2023- Du calcul des séquents à la logique linéaire Pablo Donato · 30min
- Correspondance de Curry-Howard et théorie des types Davide Barbarossa · 30min
- Réseaux de preuve multiplicatifs avec règle daemon Adrien Ragot · 30min
- Introduction à la géométrie de l'interaction originale de Girard Boris Eng · 30min
- Introduction à la syntaxe transcendantale Sidney Congard · 30min
-
Freedom and Control in Logic and Computation
February 1, 2023- Apodictic and Epidictic in Girard's transcendental syntax. Control over computation (synchronicity, sequentiality, direction of computation).
-
Proof-nets and Deep Inference
April 27, 2022- Comparison between deep inference and proof-nets. Non-sequentialisable multiplicative connectives, ludics, proof assistants, sequent calculi as recipes for computational objects (constellations).
-
Computation and Meaning
March 23, 2022- Discussion on stellar resolution and ways to put meaning on it (Girard's "usine" and "usage"), correctness criterion, realisability theory.
-
Lambda-calculus and stellar resolution
March 9, 2022- Discussion on possible encodings of lambda-calculus and Lafont's interaction nets with unification (by using stellar resolution). Decomposition of tests as constellations. Discussions on optimal reduction of lambda-calculus.
-
Round table discussion at CIRM's "Logic and Interaction" thematic month
February 2022- Discussions on Girard's transcendental syntax. Focus on Girard's "conceptual knitting".