Add Pierre's presentation
This commit is contained in:
parent
7561cd47ba
commit
1f39ad1d87
|
|
@ -4,8 +4,8 @@ title: "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.
|
||||
+ (Soon)
|
||||
- **"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"](/documents/cardascia-01-11-2024.pdf), 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).
|
||||
|
|
@ -24,7 +24,7 @@ Some meetings were private and informal. For these reasons, they are not recorde
|
|||
+ "Du calcul des séquents à la logique linéaire", Pablo Donato (30min)
|
||||
+ "Correspondance de Curry-Howard et théorie des types", Davide Barbarossa (30min)
|
||||
+ "Réseaux de preuve multiplicatifs avec règle daemon", Adrien Ragot (30min)
|
||||
+ ["Introduction à la géométrie de l'interaction originale de Girard"](/documents/slides_tc1_2023.pdf), Boris Eng (30min)
|
||||
+ ["Introduction à la géométrie de l'interaction originale de Girard"](https://engboris.fr/documents/slides_tc1_2023.pdf), Boris Eng (30min)
|
||||
+ "Introduction à la syntaxe transcendantale", Sidney Congard (30min)
|
||||
- **"Freedom and Control in Logic and Computation"** (February 1st, 2023) (4 people).
|
||||
+ Apodictic and Epidictic in Girard's transcendental syntax. Control over computation (synchronicity, sequentiality, direction of computation).
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ title: "Members"
|
|||
- [Boris Eng 🦖](https://www.engboris.fr) (administrator, coordinator)<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
|
||||
# Members
|
||||
|
||||
- [Pierre Cardascia 🎲](https://suboptimal.games/)<div class="desc-box">Philosophy, Game Design, Entrepreneurship, Immersive Experience, Poetry -- SubOptimal Games (private company)</div>
|
||||
- Baptiste Chanus<div class="desc-box">Descriptive complexity -- Université Paris 1 Panthéon-Sorbonne</div>
|
||||
|
|
@ -21,7 +21,7 @@ title: "Members"
|
|||
- 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">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>
|
||||
- [Vincent Moreau](https://www.irif.fr/~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>
|
||||
|
||||
|
|
|
|||
|
|
@ -2,25 +2,20 @@
|
|||
title: "Projects"
|
||||
---
|
||||
|
||||
# Reading/working group
|
||||
# Reading
|
||||
|
||||
## Normalisation by Evaluation (NbE)
|
||||
## >> Normalisation by Evaluation (NbE)
|
||||
|
||||
Participants: Vincent Moreau, Ambroise Lafont, Tito, Valentin Maestracci,
|
||||
Sidney Congard.
|
||||
|
||||
## Reading of Kant (Ended)
|
||||
## >> Wittgenstein's "De la certitude"
|
||||
|
||||
Participants: Ambroise Lafont, Sidney Congard, Jérémy Hervé, Luc Pommeret, Paul
|
||||
Séjourné.
|
||||
Participants: Vincent Moreau, Tito, Boris Eng, Sidney Congard.
|
||||
|
||||
## Reading of Wittgenstein (soon)
|
||||
# Development of Girard's Transcendental Syntax
|
||||
|
||||
Participants (tbc): Vincent Moreau, Tito, Boris Eng, Sidney Congard.
|
||||
|
||||
# Developement of Girard's Transcendental Syntax
|
||||
|
||||
## A programming guide to transcendental syntax
|
||||
## >> A programming guide to transcendental syntax
|
||||
|
||||
<div class="desc-box">Participants: Boris Eng.</div>
|
||||
The goal is to develop a programming guide (in the idea of Software Foundations
|
||||
|
|
@ -29,24 +24,31 @@ accessible. Eng's implementation of stellar resolution, named LSC (Large Star
|
|||
Collider) will be used for that purpose. Exercises (with solutions) have to be
|
||||
designed to open the development of transcendental syntax to contributions.
|
||||
|
||||
## A graphical user interface for stellar resolution
|
||||
[https://tsguide.refl.fr](https://tsguide.refl.fr)
|
||||
|
||||
<div class="desc-box">Participants: Pablo Donato</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.
|
||||
## >> A new manifest for transcendental syntax
|
||||
|
||||
## Tunes OS: a reflexive operating system
|
||||
<div class="desc-box">Participants: Boris Eng.</div>
|
||||
Writing of a roadmap for transcendental syntax with an analysis of various
|
||||
fields of logic and computation and several links with other fields. The point
|
||||
is to show that transcendental syntax is actually a rich subject.
|
||||
|
||||
<div class="desc-box">Participants: Jérémy Hervé, Faré.</div>
|
||||
(Soon)
|
||||
## >> Tunes OS: a reflexive operating system
|
||||
|
||||
## Some vague ideas to explore
|
||||
<div class="desc-box">Participants: Jérémy Hervé, Faré.</div>
|
||||
Exploration of the idea of a reflexive operating system which would be based
|
||||
of a minimal and reliable kernel of computation and which should be able to
|
||||
perform navigation and alteration between several levels of abstraction within
|
||||
a same system. Investigate on whether transcendental syntax can be involved
|
||||
here.
|
||||
|
||||
- Stellar resolution for symbolic execution
|
||||
- Metalanguages for stellar resolution
|
||||
- Local synchronisation of stars
|
||||
# Past activities
|
||||
|
||||
## >> Reading of Kant
|
||||
|
||||
Participants: Ambroise Lafont, Sidney Congard, Jérémy Hervé, Luc Pommeret, Paul
|
||||
Séjourné.
|
||||
|
||||
## >> Reading and comments on Krivine's "Les décompilateurs"
|
||||
|
||||
By Boris Eng.
|
||||
|
|
|
|||
Binary file not shown.
Loading…
Reference in New Issue