# 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

## Community

- Zulip chat for discussions (please ask an organiser for registration)
- Gitea for collaborative works

## Next meetings

(Soon)

## Past meetings

Full program and slides of our meetings

- “Program verification with Rust” (June 26th, 2023) by Xavier Denis.
- “Logic and quantum computation” (May 31th, 2023) by Kostia Chardonnet.
- “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

- La logique face à l’arbitraire – Sidney Congard
- nLab page on Transcendental Syntax – Boris Eng
*“A gentle introduction to Girard’s Transcendental Syntax for the linear logician”*– Boris Eng*“On Transcendental syntax: a Kantian program for logic?”*– V. Michele Abrusci & Paolo Pistone*“Towards a resource based approximation theory of programs” (PhD thesis, section 5.3)*– Davide Barbarossa

## Relevant resources

*“Information, Processes and Games” (section 1 & 5)*– Samson Abramsky*“Les limites de la correspondance preuve/programme” (French)*– Laurent Regnier*“Aristote et l’électricien : le branchement des idées” (French video)*– Paolo Pistone*“D’une logique à l’autre” (French video)*– Laurent Regnier*“Symmetry and interactivity in Programming”*– Pierre-Louis Curien*“Radical anti-realism and substructural logics”*– Jacques Dubucs & Mathieu Marion*“Which Logic for the Radical Anti-Realist?”*– Denis Bonnay & Mikaël Cozic*“Rule-Following and the Limits of Formalization: Wittgenstein’s Considerations Through the Lens of Logic” – Paolo Pistone*

## Sponsors

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