52 lines
1.8 KiB
Markdown
52 lines
1.8 KiB
Markdown
---
|
|
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
|
|
|
|
<div class="desc-box">Participants: Boris Eng.</div>
|
|
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
|
|
|
|
<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.
|
|
|
|
## Tunes OS: a reflexive operating system
|
|
|
|
<div class="desc-box">Participants: Jérémy Hervé, Faré.</div>
|
|
(Soon)
|
|
|
|
## Some vague ideas to explore
|
|
|
|
- Stellar resolution for symbolic execution
|
|
- Metalanguages for stellar resolution
|
|
- Local synchronisation of stars |