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

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

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 the theory of communication, pi-calculi, multiparty session types and their formalisation in proof assistants.

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 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.