Curry-Howard pour la concurrence – CHOCO

Le but du projet est d'étendre aux programmes concurrents et parallèles (typiquements, ceux qui sont représentés dans les algèbres de processus comme le pi-calcul), la correspondance de Curry-Howard, qui établit un isomorphisme entre programmes et preuves. A cette fin, on utilisera des progrès récents accomplis en logique et en informatique théorique: introduction de la logique linéaire différentielle, et développements en sémantique causale des programmes concurrents, dont on comprends mieux les liens avec les jeux et la ludique. ...