You may also like to check my DBLP page, or my Google Scholar page.

Intuitionistic Non-normal Modal Logics: A General Framework
Tiziano Dalmonte, Charles Grellois, Nicola Olivetti. Journal of Philosophical Logic, 2020.
On the Termination Problem for Probabilistic Higher-Order Recursive Programs
Naoki Kobayashi, Ugo Dal Lago, Charles Grellois. LMCS, 2020. Long version of the LICS 2019 paper.
Probabilistic Termination by Monadic Affine Sized Typing
Ugo Dal Lago, Charles Grellois. ACM TOPLAS, 2019. Long version of the ESOP 2017 paper.

Terminating Calculi and Countermodels for Constructive Modal Logics
Tiziano Dalmonte, Charles Grellois, Nicola Olivetti. TABLEAUX 2021.
Proof Systems for the Logics of Bringing-It-About
Tiziano Dalmonte, Charles Grellois, Nicola Olivetti. DEON 2020/2021.
On the Termination Problem for Probabilistic Higher-Order Recursive Programs
Naoki Kobayashi, Ugo Dal Lago, Charles Grellois. LICS 2019.
Linearity in higher-order recursion schemes
Pierre Clairambault, Charles Grellois, Andrzej S. Murawski. POPL 2018. Long version on demand. See also the video recording of the presentation.
Probabilistic Termination by Monadic Affine Sized Typing
With Ugo dal Lago. ESOP 2017. See also the long version.
Relational semantics of linear logic and higher-order model checking
With Paul-André Melliès. CSL 2015.
Finitary semantics of linear logic and higher-order model-checking
With Paul-André Melliès. MFCS 2015.
An infinitary model of linear logic
With Paul-André Melliès. Fossacs 2015.

Indexed linear logic and higher-order model checking
With Paul-André Melliès. Proceedings Seventh Workshop on Intersection Types and Related Systems (ITRS), 2014.

Systèmes de preuve pour les logiques de "Bringing-it-About"
Tiziano Dalmonte, Charles Grellois, Nicola Olivetti. Journées d’Intelligence Artificielle Fondamentale 2021.

Semantics of linear logic and higher-order model-checking
PhD thesis, supervised by Paul-André Melliès and Olivier Serre. 2016.

During my studies, I have also written several surveys about theoretical computer science and mathematics:

Algebraic theories, monads, and arities
It is essentially connected to Melliès's article named Segal condition meets computational effects, and introduces all the notions necessary to understand it.
Categorical interpretation of regular trees
We study the categorical and equational properties of recursion(in French).
Game semantics and higher-order model-checking
My first steps in the field. This survey relates the early proofs of Ong's decidability theorem for MSO model-checking for functional languages, modelled by higher-order recursion schemes. The draft higher in this page is an extended French version of this thesis.