Update
This commit is contained in:
parent
793ecb7b77
commit
dd8fc1a10d
|
|
@ -12,13 +12,14 @@ paige:
|
|||
#paige-title {
|
||||
font-size: 5rem;
|
||||
}
|
||||
title: "ReFL"
|
||||
---
|
||||
|
||||
<!-- {{% paige/image alt="Landscape" breakpoints=true class="object-fit-cover rounded-4 shadow-lg" fetchpriority="high" height="20rem" loading="eager" process="webp" src="https://images.unsplash.com/photo-1490604001847-b712b0c2f967?w=1296" width="100%" %}}
|
||||
|
||||
<br /><br /> -->
|
||||
|
||||
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
|
||||
|
||||
<br />
|
||||
<p style="font-size: 18px;"><a style="margin-right: 20px;" href="https://zulip.com/"><img src="/images/zulip.png"></a>
|
||||
Sponsored by Zulip. Zulip is an open-source modern team chat app designed to keep both live and asynchronous conversations organized.</p>
|
||||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -5,9 +5,9 @@ title: "Members"
|
|||
# Co-founders
|
||||
|
||||
- [Davide Barbarossa](https://davidebarbarossa12.github.io/index.html)<div class="desc-box">Lambda-calculus, type theory, linear logic, category theory, classical realizability, philosophy of mathematics -- Università di Bologna</div>
|
||||
- [Pablo Donato 🌸](http://www.lix.polytechnique.fr/Labo/Pablo.DONATO/) (administrator)<div class="desc-box">Sequent calculus, deep inference, type theory, Peirce's existential graphs, focalization, proof search -- Ecole Polytechnique</a>
|
||||
- [Pablo Donato 🌸](http://www.lix.polytechnique.fr/Labo/Pablo.DONATO/) (administrator)<div class="desc-box">Sequent calculus, deep inference, type theory, Peirce's existential graphs, focalization, proof search -- Ecole Polytechnique (LIX)</a>
|
||||
- [Boris Eng 🦖](https://www.engboris.fr) (administrator)<div class="desc-box">Computer science, transcendental syntax -- OCamlPro / SuperBOL</a>
|
||||
- Valentin Maestracci<div class="desc-box">Lambda-calculus, type theory, homotopy type theory, Dedukti, directed homotopy theory, rewriting -- Université Aix-Marseille</a>
|
||||
- [Valentin Maestracci](https://vmaestracci.github.io/)<div class="desc-box">Lambda-calculus, type theory, homotopy type theory, Dedukti, directed homotopy theory, rewriting -- Université Aix-Marseille</a>
|
||||
|
||||
# Members
|
||||
|
||||
|
|
@ -15,10 +15,10 @@ title: "Members"
|
|||
- [Kostia Chardonnet](https://kostiachardonnet.github.io/)<div class="desc-box">Computer science, quantum computation, cyclic proofs -- Centre Inria de l'Université de Lorraine (MOCQUA)</div>
|
||||
- [Sidney Congard](https://dwarfobserver.github.io/)<div class="desc-box">Semantics of programming languages -- Centre Inria de l'Université de Rennes (Galinette)</div>
|
||||
- Jérémy Hervé 🍄<div class="desc-box">Mushrooms -- Independent</div>
|
||||
- [Ambroise Lafont](https://amblafont.github.io/)<div class="desc-box">Type Theory and Category Theory -- University of Cambridge</div>
|
||||
- Luc Pommeret
|
||||
- [Ambroise Lafont](https://amblafont.github.io/)<div class="desc-box">Type Theory and Category Theory -- École Polytechnique (LIX)</div>
|
||||
- Luc Pommeret<div class="desc-box">Logic, LLM (Machine learning) -- Université Paris Cité (IRIF)</div>
|
||||
- Adrien Ragot<div class="desc-box">Proof-nets, interaction nets, implicit computational complexity, lambda-calculus, linear logic -- Université Sorbonne Paris Nord / University Roma Tre</div>
|
||||
- Paul Séjourné<div class="desc-box">Philosophy (Aristotle, Kant, Deleuze), algebraic geometry, category theory -- Université Paris-Sorbonne</div>
|
||||
- Paul Séjourné<div class="desc-box">Archaic and contemporary philosophy (of mathematics), algebraic geometry, category theory -- Université Paris-Sorbonne</div>
|
||||
- Vincent Moreau<div class="desc-box">Category theory, type theory, denotational semantics, topology, algebra, proof assistants -- Université Paris Cité (IRIF)</div>
|
||||
- [Tito](https://nguyentito.eu/)<div class="desc-box">Links between linear logic and automata theory, combinatorics, computational complexity, algorithms -- École normale supérieure de Lyon</div>
|
||||
- [Xavier Denis](https://xav.io/)<div class="desc-box">Deductive verification and specification of Rust programs -- ETH Zurich</div>
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
Loading…
Reference in New Issue