1.8 KiB
1.8 KiB
| title |
|---|
| Projects |
Reading/working group
Normalisation by Evaluation (NbE)
Participants: Vincent Moreau, Ambroise Lafont, Tito, Valentin Maestracci, Sidney Congard.
Reading of Kant (Ended)
Participants: Ambroise Lafont, Sidney Congard, Jérémy Hervé, Luc Pommeret, Paul Séjourné.
Reading of Wittgenstein (soon)
Participants (tbc): Vincent Moreau, Tito, Boris Eng, Sidney Congard.
Developement of Girard's 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
for Coq) in order to make the ideas of Girard's transcendental syntax more
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
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.
Tunes OS: a reflexive operating system
Participants: Jérémy Hervé, Faré.
(Soon)
Some vague ideas to explore
- Stellar resolution for symbolic execution
- Metalanguages for stellar resolution
- Local synchronisation of stars