Lorenzo Gheri

Lorenzo Gheri
Office: S2|02 E312
Phone: +49 6151 16-25253
Fax: +49 6151 16-25251
Mail: gheriatmais.informatik.tu-darmstadt.de

TU Darmstadt

Department of Computer Science

Modeling and Analysis of Information Systems

Hochschulstraße 10

D-64289 Darmstadt


Short Bio

I am a research assistant (postdoc) within the MAIS group, lead by Prof. Heiko Mantel, at the Technical University of Darmstadt. My main research topic at MAIS is information flow security and its applications to static analysis of program code, with particular focus on concurrency aspects.

Formerly, I was conducting a PhD project at the Foundations of Computing group, Middlesex University London, supervised by Rajagopal Nagarajan, Andrei Popescu (Director of Studies) and Franco Raimondi. My thesis ("A General Theory of Syntax with Bindings") was submitted in September 2018, defended on the 31st of January 2019 with a positive outcome, conditional to "minor revision and corrections". These are currently being processed.

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.

Research Interests

  • Information flow security
  • Syntax with bindings
  • Programming languages
  • Mathematical logic
  • Formal methods
More in general, I come from a pure mathematical background and got interested in the theory of computer science. Thus, I enjoy reasoning about different problems from theoretical computer science, mathematical logic, abstract algebra and the foundations of mathematics. During my Master studies I fell in love with proof assistants, I still am and, although this is no country for monogamy, Isabelle/HOL has got a special place in my heart.

Drafts, Publications and Formal Proof Developments

All drafts, publications and formal proof developments are available at: https://sites.google.com/view/lorgheri/research


  • Lorenzo Gheri, Andrei Popescu. A Formalized General Theory of Syntax with Bindings. Draft. Extended Version for a journal publication of our conference paper with the same name.
  • Lorenzo Gheri, Andrei Popescu. A Case Study in Reasoning about Syntax with Bindings: The Church-Rosser and Standardization Theorems. Draft. For a journal publication.


  • Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel. Bindings as Bounded Natural Functors. In Weirich, S. (ed.) 46th ACM SIGPLAN Symposium on Principles of Programming Language (POPL 2019), ACM, 2019, Article 22, pp. 22:1–22:34
  • Lorenzo Gheri, Andrei Popescu. A Formalized General Theory of Syntax with Bindings. In: ITP 2017. LNCS 10499, 241-261, Springer.

Formal Proof Developments

  • Lorenzo Gheri, Andrei Popescu. A General Theory of Syntax with Bindings. In: Archive of Formal Proofs, 2019.

A A A | Print | Imprint | Sitemap | Contact
zum Seitenanfang