diff --git a/content/_index.md b/content/_index.md index c1e873c..b0c5f9b 100644 --- a/content/_index.md +++ b/content/_index.md @@ -12,13 +12,14 @@ paige: #paige-title { font-size: 5rem; } +title: "ReFL" --- -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 relectures 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. +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. @@ -44,5 +45,6 @@ Our Zulip chat: [chat.refl.fr](http://chat.refl.fr) # Sponsors +

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

\ No newline at end of file diff --git a/content/meetings.md b/content/meetings.md index 243f8a7..da30207 100644 --- a/content/meetings.md +++ b/content/meetings.md @@ -4,6 +4,13 @@ title: "Meetings" Some meetings were private and informal. For these reasons, they are not recorded here. +- **"Analytic and continental philosophy"** (End of May, 2024) by Luc Pommeret. + + (TBA), Luc Pommeret (1h30) +- **"Program verification"** (June 26th, 2023) by Xavier Denis. + + "Presentation of the Rust programming language", Xavier Denis (1h) + + "Why formal verification is getting it wrong", Xavier Denis (1h) +- **"Logic and quantum computation"** (May 31th, 2023) by Kostia Chardonnet. Chair: Kostia Chardonnet. + + "Quantum computation and Geometry of Interaction", Kostia Chardonnet (45min) - **"Logic and Categories"** (March 24th, 2023) by Tito and Valentin Maestracci. Chair: Pablo Donato. + ["Pourquoi les catégories sont la bonne façon de faire de la sémantique dénotationnelle"](https://nguyentito.eu/2023-03-refl.pdf), Tito (1h) + "Catégories monoïdales à trace", Valentin Maestracci (1h) diff --git a/content/members.md b/content/members.md index d86a453..8d584b9 100644 --- a/content/members.md +++ b/content/members.md @@ -5,9 +5,9 @@ title: "Members" # Co-founders - [Davide Barbarossa](https://davidebarbarossa12.github.io/index.html)
Lambda-calculus, type theory, linear logic, category theory, classical realizability, philosophy of mathematics -- Università di Bologna
-- [Pablo Donato 🌸](http://www.lix.polytechnique.fr/Labo/Pablo.DONATO/) (administrator)
Sequent calculus, deep inference, type theory, Peirce's existential graphs, focalization, proof search -- Ecole Polytechnique +- [Pablo Donato 🌸](http://www.lix.polytechnique.fr/Labo/Pablo.DONATO/) (administrator)
Sequent calculus, deep inference, type theory, Peirce's existential graphs, focalization, proof search -- Ecole Polytechnique (LIX) - [Boris Eng 🦖](https://www.engboris.fr) (administrator)
Computer science, transcendental syntax -- OCamlPro / SuperBOL -- Valentin Maestracci
Lambda-calculus, type theory, homotopy type theory, Dedukti, directed homotopy theory, rewriting -- Université Aix-Marseille +- [Valentin Maestracci](https://vmaestracci.github.io/)
Lambda-calculus, type theory, homotopy type theory, Dedukti, directed homotopy theory, rewriting -- Université Aix-Marseille # Members @@ -15,10 +15,10 @@ title: "Members" - [Kostia Chardonnet](https://kostiachardonnet.github.io/)
Computer science, quantum computation, cyclic proofs -- Centre Inria de l'Université de Lorraine (MOCQUA)
- [Sidney Congard](https://dwarfobserver.github.io/)
Semantics of programming languages -- Centre Inria de l'Université de Rennes (Galinette)
- Jérémy Hervé 🍄
Mushrooms -- Independent
-- [Ambroise Lafont](https://amblafont.github.io/)
Type Theory and Category Theory -- University of Cambridge
-- Luc Pommeret +- [Ambroise Lafont](https://amblafont.github.io/)
Type Theory and Category Theory -- École Polytechnique (LIX)
+- Luc Pommeret
Logic, LLM (Machine learning) -- Université Paris Cité (IRIF)
- 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
+- Paul Séjourné
Archaic and contemporary philosophy (of mathematics), algebraic geometry, category theory -- Université Paris-Sorbonne
- Vincent Moreau
Category theory, type theory, denotational semantics, topology, algebra, proof assistants -- Université Paris Cité (IRIF)
- [Tito](https://nguyentito.eu/)
Links between linear logic and automata theory, combinatorics, computational complexity, algorithms -- École normale supérieure de Lyon
- [Xavier Denis](https://xav.io/)
Deductive verification and specification of Rust programs -- ETH Zurich
diff --git a/content/resources.md b/content/resources.md index 79dab79..40649c9 100644 --- a/content/resources.md +++ b/content/resources.md @@ -3,6 +3,7 @@ title: "Resources" --- - [*"An exegesis of transcendental syntax" (PhD thesis)* -- Boris Eng](https://hal.science/tel-04179276v1) +- [*"La logique face à l'arbitraire" (French)* -- Sidney Congard](https://hal.science/hal-03689001/document) - [*"Information, Processes and Games" (section 1 & 5)* -- Samson Abramsky](https://arxiv.org/abs/1604.02603) - [*"Les limites de la correspondance preuve/programme" (French)* -- Laurent Regnier](https://www.i2m.univ-amu.fr/perso/laurent.regnier/articles/ch.pdf) - [*"Aristote et l’électricien : le branchement des idées" (French video)* -- Paolo Pistone](https://vimeo.com/167115532) diff --git a/hugo.toml b/hugo.toml index 056cc83..90a9353 100644 --- a/hugo.toml +++ b/hugo.toml @@ -1,4 +1,4 @@ -baseurl = "https://example.com" +baseurl = "https://refl.fr" copyright = "© ReFL, website based on Will Fraught's Paige theme for Hugo" enablerobotstxt = true languagecode = "en-us"