Lorenzo Gheri, PhD

Research Associate at the Mobility Reading Group

Department of Computing

Imperial College London


  • Department of Computing, Imperial College London, 180 Queen's Gate, South Kensington Campus, London, SW7 2AZ, United Kingdom

email contacts:

  • l.gheri(at)imperial.ac.uk

  • lor.gheri(at)gmail.com

I am a Research Associate at the Mobility Reading Group, lead by Nobuko Yoshida, Imperial College London.

Previously, I was a research assistant (Wissenschaftliche Mitarbeiter) at the MAIS research group, lead by Heiko Mantel.

I got my PhD from Middlesex University London, where I worked at the Foundations of Computing group. My thesis ("A General Theory of Syntax with Bindings") has been supervised by Rajagopal Nagarajan, Andrei Popescu (Director of Studies) and Franco Raimondi.

Before moving to London I got my BSc and MSc in pure mathematics from the University of Florence (UniversitĂ  degli Studi di Firenze), my hometown in Italy. My Master thesis was supervised by Marco Maggesi.

My current research is in concurrency and proof assistants.

I am particularly interested in the mechanisation of concurrent calculi and their type systems. I am one of the initiators of "The Concurrent Calculi Formalisation Benchmark", a project that aims at the popularisation of the topic and at fostering high-quality research in it. Also, I have been studying choreographic approaches for safe communication among multiple participants (multiparty session types, choreography automata), with focus on their expressiveness (explicit connections, delegation, design-by-contract approach) and their compositionality properties.

At TU Darmstadt, I worked on the theory of information flow security, with particular focus on concurrency aspects.

During my PhD years, I focussed on abstract syntax, with particular attention to variable binding structures. I investigated features and mechanisms common to different syntaxes, such as (co)recursion, (co)induction and (capture avoiding) substitution. I formalized the development and results of my PhD work on syntax with bindings in the Isabelle/HOL proof assistant, using techniques from category theory, nominal logic and model theory.

From a wider point of view, my research interests are programming languages, theoretical computer science, mathematical logic, formal methods, abstract algebra, and the foundations of mathematics. For my Master thesis project I worked with Coq and homotopy type theory.