Lorenzo Gheri, PhD

Associate Researcher 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

Recently I moved to Imperial College London, as a Research Assistant at the Mobility Reading Group, lead by Prof. Nobuko Yoshida.

From October 2018 until September 2019, I was employed as a research assistant (Wissenschaftliche Mitarbeiter) at the MAIS research group, lead by Heiko Mantel.

I have 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 Multiparty Session Types and in their formalization in proof assistants.

At TU Darmstadt, my research interests have been extended to the theory of information flow security, with particular focus on concurrency aspects.

My main research topic has been, up to now, abstract syntax, with particular attention to variable binding structures. I have investigated features and mechanisms common to different syntaxes, such as (co)recursion, (co)induction and (capture avoiding) substitution.

I have formalized the development and results of my PhD work on syntax with bindings in the Isabelle/HOL proof assistant, using mainly 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.