Lambda-calculus, type theory, homotopy type theory, Dedukti, directed homotopy theory, rewriting -- Université Aix-Marseille
-# Members
+# Members
- [Pierre Cardascia 🎲](https://suboptimal.games/)
Philosophy, Game Design, Entrepreneurship, Immersive Experience, Poetry -- SubOptimal Games (private company)
- Baptiste Chanus
Descriptive complexity -- Université Paris 1 Panthéon-Sorbonne
@@ -21,7 +21,7 @@ title: "Members"
- 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é
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)
+- [Vincent Moreau](https://www.irif.fr/~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/projects.md b/content/projects.md
index ada6121..656f270 100644
--- a/content/projects.md
+++ b/content/projects.md
@@ -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
Participants: Boris Eng.
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)
-
Participants: Pablo Donato
-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
+
Participants: Boris Eng.
+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.
-
Participants: Jérémy Hervé, Faré.
-(Soon)
+## >> Tunes OS: a reflexive operating system
-## Some vague ideas to explore
+
Participants: Jérémy Hervé, Faré.
+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
\ No newline at end of file
+# 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.
diff --git a/static/documents/cardascia-01-11-2024.pdf b/static/documents/cardascia-01-11-2024.pdf
new file mode 100644
index 0000000..a288fc3
Binary files /dev/null and b/static/documents/cardascia-01-11-2024.pdf differ