ReFL / Réflexions sur les Fondements de la Logique
French discussion group on the foundations of logic and computation. The group was initially founded by four PhD students during the “Linear Logic Winter School 2022” but we now aim for a broader group where discussions can be created between logicians, computer scientists, mathematicians, philosophers and more, with various backgrounds and profiles, with the aim of proposing original insights and relectures of the foundations of computation and logic. In particular, we put a special attention on the role of computer science in the understanding of logic.
Our scientific interests are the following:
- foundations and philosophy of logic, computation and mathematics
- history of logic and computation
- alternative conceptions and architectures for logic and computation
- category theory and its applications
- proof-program correspondence, proof/type theory, lambda-calculus, realizability theory
- linear logic, proof-nets, ludics, geometry of interaction, transcendental syntax
Our activities include:
- open seminars (generally online)
- debates and discussions on Zulip
- private (but transparent, see below) meetings in person between some participants
- help for technical questions or references related to our scientific interests
- production of papers
We are inspired by the transdisciplinarity of the LIGC working group which gathered researchers from various fields around the foundations of (linear) logic.
For the moment, our discussions are in French but we still offer a space for discussions in English and are open to communication in English. The official language of our discussions may change to English depending on the number of English speakers among regular participants.
Members
Co-founders & organisers (4)
- Davide Barbarossa
Lambda-calculus, type theory, linear logic, category theory, classical realizability, philosophy of mathematics – Università di Bologna
- Pablo Donato
Sequent calculus, deep inference, type theory, Peirce’s existential graphs, focalization, proof search – Ecole Polytechnique
- Boris Eng
Computer science, technical side of the transcendental syntax – Université Sorbonne Paris Nord
- Valentin Maestracci
Lambda-calculus, type theory, homotopy type theory, Dedukti, directed homotopy theory, rewriting – Université Aix-Marseille
Regular participants (10)
- Baptiste Chanus
Descriptive complexity – Université Paris 1 Panthéon-Sorbonne
- Kostia Chardonnet
Computer science, quantum computation, cyclic proofs – Université Paris Saclay
- Sidney Congard
Computer science, Verification – Université Paris Cité
- Jérémy Hervé
- Julien Marquet
Formal mathematics, verification, type systems, Nix, DevOps – ENS Ulm
- Ambroise Lafont
Type Theory and Category Theory – University of Cambridge
- Adrien Ragot
Proof-nets, interaction nets, implicit computational complexity, lambda-calculus, linear logic – Université Sorbonne Paris Nord / University Roma Tre
- Paul Séjourné
Philosophy (Aristotle, Kant, Deleuze), algebraic geometry, category theory – Université Paris-Sorbonne
- Tito
Links between linear logic and automata theory, combinatorics, computational complexity, algorithms – École normale supérieure de Lyon
- Xavier Denis
Deductive verification and specification of Rust programs – Université Paris-Saclay
Visitors (13)
- Hugo Cadière
Philosophy of German idealism (Kant, Hegel, Fichte) and inferantialism (Brandom, Sellars) – Université Lyon 3
- Titouan Carette
Mathematics, quantum computation – Université Paris Saclay
- Clémence Chanavat
Category theory, directed algebraic topology, diagrammatic sets – Université Paris-Saclay
- Aloÿs Dufour
Category theory, lambda-calculus, categorical semantics, type systems, linear logic, algebraic geometry, homotopy theory – Université Sorbonne Paris Nord
- Yannis Hausberg
Philosophy of science – Université Lyon 3
- Axel Kerinec
Lambda-calculus, linear logic, type theory – Université Sorbonne Paris Nord
- Bernardo Marques
- Vincent Moreau
- Rémi Nollet
Computer science, cyclic proofs
- Federico Olimpieri
Computer science, type theory – University of Leeds
- Raphael Tossings
History of modern philosophy (Descartes, Kant, Hegel), Brandom, analytical philosophy – Sorbonne University & Ottawa University
- Pierre Vial
Metaprogramming in Coq, proof assistants, quantitative intersection type systems, infinitary calculi and coinduction, Lambda-Mu calculus, Semantics of the pure lambda-calculus – ENS Paris-Saclay
- Quentin
- Zulip chat for discussions (please ask an organiser for registration)
- Gitea for collaborative works
Next meetings
- “Logic and quantum computation” (May 2023).
- “Program verification” (June 2023).
Past meetings
Full program and slides of our meetings
- “Logic and Categories” (March 24th, 2023) by Tito and Valentin Maestracci.
- “ReFL first seminar of the year” (February 21, 2023) by Pablo Donato, Davide Barbarossa, Adrien Ragot, Boris Eng, Sidney Congard (around 13 people online).
- “Freedom and Control in Logic and Computation” (February 1st, 2023) (4 people).
- “Proof-nets and Deep Inference” (April 27, 2022) by Pablo Donato (5 people).
- “Computation and Meaning” (March 23, 2022) by Boris Eng (8 people).
- “Lambda-calculus and stellar resolution” (March 9, 2022) by Boris Eng and Julien Marquet (6 people).
- Round table discussion at CIRM’s “Logic and Interaction” thematic month (February 2022) (8 people).
References on Girard’s Transcendental Syntax
Relevant resources

Sponsored by Zulip. Zulip is an open-source modern team chat app designed to keep both live and asynchronous conversations organized.