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 (8)

• Baptiste Chanus
  Descriptive complexity – Université Paris 1 Panthéon-Sorbonne
• 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

Visitors (13)

• Kostia Chardonnet
  Computer science, quantum computation, cyclic proofs – Université Paris Saclay
• 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
• 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
• Xavier Denis
  Deductive verification and specification of Rust programs – Université Paris-Saclay

Community

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

Next meetings

• “Logic in programming, verification and operating systems” (April 2023).
• “Logic and Quantum Computation” (May 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

• 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.