Main Achievements
Multitoken Machines
We have developed a fully-fledged multitoken machine for a very powerful
logical systems in which not only exponentials, but also a very general notion of fixpoint can be
expressed. This has been done jointly by Dal Lago, Faggian and Valiron (from the french side)
and Yoshimizu (from the japanese side). Noticeabily, this has been published
[LICS2015] in the
proceedings of LICS 2015, the flagship conference in logic in computer science.
Graded Monads
We have initiated a study of graded monads as a way to generalise and extend the
classic monadic theory, involving both the PI.R2 and the RIMS-CS sites
[FoSSaCS2016].
Multitoken Machines and Concurrency
Multitoken Machines and Concurrency. We studied how much of the multitoken paradigm can be
adapted to concurrent languages. We have introduced a geometry of interaction model for multiport
interaction combinators, themselves a very powerful model of concurrent interaction. The model has
been proved sound and adequate with respect to multiport combinators reduction. A paper presenting
these results by three project members from FoCUS and MMM has
been published in the proceedings of a well-established conference in the field
[LICS2017].
Dealing with Quantum and Probabilistic Effects in Multitoken Machines
The multitoken paradigm has been shown to be applicable to
probabilistic and quantum contexts, by project members from FoCUS, MMM, and PI.R2.
This has been published
[POPL2017] in a
leading conference in the field of programming language theory.