I started my journey in the field with Dr Paul-André Melliès (CNRS), my primary PhD supervisor. My  secondary supervisor was Dr Olivier Serre (CNRS).

Functional programs are such that a function can take another function as input. This creates significant challenges when it comes to their mathematical analysis. We have revisited and enhanced existing proofs and techniques for the analysis of functional programs, bringing them to fully structured algebraic frameworks (extensions of models of linear logic). 

This led us to the first fully compositional verification approach for that problem: via our contribution, checking that a functional program is bug-exempt can be performed component by component, then obtaining the global result by simple composition mechanisms.

That first significant experience in research has convinced me of the importance of compositionality for modeling and analysing systems: from the analysis of their sub-components, compute efficiently the behaviour of the whole.

Publications: ITRS 2014, FoSSaCS 2015, CSL 2015, MFCS 2015 + my PhD thesis.

Further refinements in the field, at the light of linear logic and related typing disciplines, were explored with Prof Andrzej Murawski (Oxford) and Dr Pierre Clairambault (CNRS).

Publication: POPL 2018.

More technically. During my postdoc with Prof Ugo Dal Lago (Bologna), we designed a type system that ensures that a probabilistic functional program that is typeable will terminate with probability 1.

In other words, the problem might not terminate in some cases, but the set of non-terminating executions must have measure 0: non-termination is improbable, not impossible.

Publications: ESOP 2017, ACM TOPLAS 2019.

We then teamed with Prof Naoki Kobayashi (Tokyo) to investigate further questions of probablistic termination for functional programs, extended with probabilistic choice, in a framework derived from higher-order recursion schemes.

Publications: LICS 2019, LMCS 2020.