During our study of higher-order model-checking (with Mellies), we rooted our analysis on linear logic and its semantics.
Linear logic enables one to precisely describe the use of resources during a computation, and we enriched the framework with information about the verification of properties, resulting in models in which the mathematical interpretation of a problem solves the verification problem under study.
This led us to extending the relational semantics with infinitary constructions, and with parity games.
Main publication: FoSSaCS 2015. See also my PhD thesis.
During my first Lectureship in Aix-Marseilles University, I started working with Prof Nicola Olivetti on modal logics, a welcome extension to my logical portfolio.
We started by an in-depth study of non-normal modal logics, in the intuitionnistic setting. We proved the existence of 24 distinct bimodal logics, studying both the proof theory and the semantics and each of them in a unified framework.
We then did further work on constructive modal logics, and on more specific logics such as deontic logics and the logics of Bringing-It-About.
Publications: Journal of Philosophical Logic 2020, TABLEAUX 2021, DEON 2020/2021, WoLLIC 2022, Journal of Logic and Computation 2024.