Dr Charles Grellois

Charles studied mathematics and theoretical computer science at the École Normale Supérieure de Cachan and obtained his PhD from Université Paris Diderot in 2016. Before joining Sheffield in 2023, he was a postdoctoral researcher in Bologna and held Maître de Conférences positions in Aix-Marseille and Bordeaux.

His core research is in the semantics and verification of programs, especially functional programs. He uses tools from denotational semantics, type theory, linear logic, fixed-point theory, modal logics and higher-order model checking to reason about program behaviour, both in deterministic and probabilistic settings.

A second strand of his work applies mathematical and computational modelling to complex biological and medical systems. In collaboration with colleagues in neuroscience, medicine and oncology, he studies how formal, dynamical and machine-learning models can help describe systems such as neuro-metabolic dysfunction, Alzheimer’s disease and cancer evolution. Across these areas, his research is motivated by a common question: how can compositional mathematical structures help us understand, verify and control complex systems?

Charles also leads an ARIA-backed Innovator Circle, currently investigating modular aspects of neural structures and how this could benefit to energy-friendly machine learning but also to brain modelling for medical or neuroscientific applications.