Update
This commit is contained in:
parent
dd8fc1a10d
commit
cedaa78670
|
|
@ -41,7 +41,7 @@ Our Zulip chat: [chat.refl.fr](http://chat.refl.fr)
|
|||
- debates and discussions on Zulip
|
||||
- private meetings in person between some participants
|
||||
- collaboration and mutual assistance (thesis, research, software, programming, ...)
|
||||
- writing, communication
|
||||
- writing, communication, programming projects
|
||||
|
||||
# Sponsors
|
||||
|
||||
|
|
|
|||
|
|
@ -4,8 +4,12 @@ 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.
|
||||
- **"Analytic and continental philosophy"** (May 20th, 2024) by Luc Pommeret.
|
||||
+ (TBA), Luc Pommeret (1h30)
|
||||
- **"Technical introduction to transcendental syntax"** (May 11th, 2024) (4 people).
|
||||
+ "Introduction to Peirce's philosophy", Pablo Donato (30min).
|
||||
+ "Stellar resolution and Girard's knitting", Boris Eng.
|
||||
- **"Meeting around Jean-Yves Girard"** (May 10th, 2024) (5 people).
|
||||
- **"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)
|
||||
|
|
|
|||
|
|
@ -5,8 +5,8 @@ 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 (LIX)</a>
|
||||
- [Boris Eng 🦖](https://www.engboris.fr) (administrator)<div class="desc-box">Computer science, transcendental syntax -- OCamlPro / SuperBOL</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)</div>
|
||||
- [Boris Eng 🦖](https://www.engboris.fr) (administrator)<div class="desc-box">Transcendental syntax, computer science -- OCamlPro (private company)</div>
|
||||
- [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
|
||||
|
|
@ -14,7 +14,7 @@ title: "Members"
|
|||
- Baptiste Chanus<div class="desc-box">Descriptive complexity -- Université Paris 1 Panthéon-Sorbonne</div>
|
||||
- [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>
|
||||
- Jérémy Hervé 🍄<div class="desc-box">Mushrooms, operating systems design -- Independent</div>
|
||||
- [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>
|
||||
|
|
@ -25,4 +25,4 @@ title: "Members"
|
|||
|
||||
# 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.
|
||||
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.
|
||||
|
|
@ -2,4 +2,31 @@
|
|||
title: "Projects"
|
||||
---
|
||||
|
||||
(Soon...)
|
||||
# Developement of Girard's Transcendental Syntax
|
||||
|
||||
## La syntaxe transcendantale, manuel (in French)
|
||||
|
||||
<div class="desc-box">Participants : Boris Eng.</div>
|
||||
Bien que l'esprit et la philosophie de la syntaxe transcendantale arrivent à
|
||||
se diffisuer, il y a un manque flagrant : il est difficile de s'approprier les
|
||||
objets de la syntaxe transcendantale et de les manipuler. Cela est plus dû au
|
||||
manque de ressources qu'à la complexité des concepts. Nous proposons donc un
|
||||
manuel pratique et ludique avec des exercices. Il est nécessaire de se
|
||||
familiariser avec la technique afin de pouvoir réfléchir à des façons originales
|
||||
de répondre à des problèmes de syntaxe transcendantale.
|
||||
|
||||
## A graphical user interface for stellar resolution
|
||||
|
||||
<div class="desc-box">[Not assigned]</div>
|
||||
In order to explain how stellar resolution works in a more convenient way, it
|
||||
would be better to have a graphical interface in which it is possible to: add
|
||||
stars to a constellation (reference constellation in Eng's thesis), put stars in
|
||||
an interaction space, manually select stars from the reference constellation and
|
||||
make them interact in the interaction space (possible interactions must be
|
||||
displayed before actually triggering the interaction). Another possible feature
|
||||
is to manually construct diagrams and apply fusion steps.
|
||||
|
||||
## Tunes OS: a reflexive operating system
|
||||
|
||||
<div class="desc-box">Participants: Jérémy Hervé.</div>
|
||||
(Soon)
|
||||
|
|
@ -2,9 +2,9 @@
|
|||
title: "Resources"
|
||||
---
|
||||
|
||||
- *"Le fantôme de la transparence"* -- Jean-Yves Girard
|
||||
- [*"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)
|
||||
- [*"D'une logique à l'autre" (French video)* -- Laurent Regnier](https://vimeo.com/314743657)
|
||||
|
|
|
|||
|
|
@ -40,6 +40,10 @@ a {
|
|||
color: rgb(40, 173, 145);
|
||||
}
|
||||
|
||||
a:hover {
|
||||
opacity: 0.5;
|
||||
}
|
||||
|
||||
.nav-link {
|
||||
color: rgb(40, 173, 145);
|
||||
}
|
||||
Loading…
Reference in New Issue