ReFL

Will Faught

2 minutes

French scientific network 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 initiated between logicians, computer scientists, mathematicians, philosophers and more. We have people with various backgrounds and profiles and we all share a taste for deep questions and the aim of proposing original insights and new perspectives of the foundations of computation and logic. In particular, we take a great interest in the role of computer science in the understanding of logic.

We are inspired by the transdisciplinarity of the LIGC working group which gathered researchers from various fields around the foundations of (linear) logic.

We use French for our discussions, seminars and meetings but we are open to English speakers for discussions.

Our Zulip chat: chat.refl.fr

Our mailing list: refl@framalistes.org

Our scientific interests

foundations and philosophy of logic, computation and mathematics
history of logic and computation
category theory and its applications
proof-program correspondence and proof/type theory
Jean-Yves Girard’s works: linear logic, proof-nets, ludics, geometry of interaction, transcendental syntax

Our activities

seminars (generally online)
debates and discussions on Zulip
private meetings in person between some participants
collaboration and mutual assistance (thesis, research, software, programming, …)
writing, communication, programming projects

Sponsors #

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

Collections

Authors

Will Faught

Pages

January 0001

Meetings

Some meetings were private and informal. For these reasons, they are not recorded here. “Fondements esthétiques de la logique” (November 1st, 2024) by Pierre Cardascia (16 people). “Morts du mythe, de l’art, de la philosophie, de la logique : Itinéraire d’un problème serial-killer”, Pierre Cardascia (1h30) “Analytic and continental philosophy” (May 20th, 2024) by Luc Pommeret (17 people). “Le professionnel et l’écrivain : le pouvoir offensif de la philosophie analytique”, Luc Pommeret (1h30) “Technical introduction to transcendental syntax” (May 11th, 2024) (4 people).

Will Faught

2 minutes

Members

Co-founders Davide BarbarossaLambda-calculus, type theory, linear logic, category theory, classical realizability, philosophy of mathematics – Università di Bologna Pablo Donato 🌸 (administrator)proof theory, type theory, topos theory, proof assistants, human-computer interaction, end-user programming – Grothendieck Institute Boris Eng 🦖 (administrator, coordinator)Transcendental syntax, computer science – OCamlPro (private company) Valentin MaestracciLambda-calculus, type theory, homotopy type theory, Dedukti, directed homotopy theory, rewriting – Université Aix-Marseille Members Pierre Cardascia 🎲Philosophy, Game Design, Entrepreneurship, Immersive Experience, Poetry – SubOptimal Games (private company) Baptiste ChanusDescriptive complexity – Université Paris 1 Panthéon-Sorbonne Kostia ChardonnetComputer science, quantum computation, cyclic proofs – Centre Inria de l’Université de Lorraine (MOCQUA) Sidney CongardSemantics of programming languages – Centre Inria de l’Université de Rennes (Galinette) Charles GrelloisUniversity of Sheffield Jérémy Hervé 🍄Mushrooms, operating systems design – Independent Ambroise LafontType Theory and Category Theory – École Polytechnique (LIX) Luc PommeretLogic, LLM (Machine learning) – Université Paris Cité (IRIF) Adrien RagotProof-nets, interaction nets, implicit computational complexity, lambda-calculus, linear logic – Université Sorbonne Paris Nord / University Roma Tre Paul SéjournéArchaic and contemporary philosophy (of mathematics), algebraic geometry, category theory – Université Paris-Sorbonne Vincent MoreauCategory theory, type theory, denotational semantics, topology, algebra, proof assistants – Université Paris Cité (IRIF) TitoLinks between linear logic and automata theory, combinatorics, computational complexity, algorithms – CNRS & Aix-Marseille Xavier DenisDeductive verification and specification of Rust programs – ETH Zurich Visitors and guests Hugo Cadière, Titouan Carette, Clémence Chanavat, Bernardo Marques, Julien Marquet, Rémi Nollet, Federico Olimpieri, Raphael Tossings, Pierre Vial, Quentin, Gael Deest, Martin Tricaud, Fadi Shawki, Eliès Harington, Axel Kerinec, Aloÿs Dufour, Bernardo, Anne-Laure, Escherichia, Alexey, François-René Rideau (Faré), Roman Perez, Nico.

Will Faught

2 minutes

Projects

Reading » Normalisation by Evaluation (NbE) Participants: Vincent Moreau, Ambroise Lafont, Tito, Valentin Maestracci, Sidney Congard. » Wittgenstein’s “De la certitude” Participants: Vincent Moreau, Tito, Boris Eng, Sidney Congard. Development of Girard’s Transcendental Syntax » A programming guide to transcendental syntax Participants: Boris Eng. The goal is to develop a programming guide (in the idea of Software Foundations for Coq) in order to make the ideas of Girard's transcendental syntax more accessible.

Will Faught

2 minutes

Resources

“Le fantôme de la transparence” – Jean-Yves Girard Syntaxe transcendentale (Wikipédia) Transcendental Syntax (nlab) “An exegesis of transcendental syntax” (PhD thesis) – Boris Eng “La logique face à l’arbitraire” (French) – Sidney Congard “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?

Will Faught

1 minute