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.