Marco Solieri is a research associate at the University of Bath where he works with Jim Laird and the rest of the group Mathematical foundations of computation of the Computer science department.

Previously, he obtained a joint Ph.D. between the Université Paris 13, in France, and the Università di Bologna, in Italy. In the former, he has been a member of the team Logic, Computation and Reasoning (LCR) of the Computer Science Laboratory of Paris-North University (LIPN), under the supervision of Stefano Guerrini and Michele Pagani. In the latter, he has been a collaborator of the INRIA Focus team, at the Computer Science and Engineering Department (DISI), where he has been supervised by Simone Martini. He also spent part of the last year of his doctoral activities at the Institut de Recherche en Informatique Fondamentale (IRIF) with the team Preuves, programmes et systèmes (PPS).

His main research goal is to study and develop models and techniques for the implementation and the semantics of functional languages. He thus works on the logical foundations of programming languages, proof theory, type theory and rewriting theory. In particular he employs and studies linear logics and proof nets, sharing graphs and interaction nets, geometry of interaction and optimal reduction, and lambda calculi even with resources.


In reverse chronological order.


  1. Marco Solieri, Geometry of Resource Interaction and Taylor-Ehrhard-Regnier Expansion — A Minimalist Approach.
  2. Marco Solieri, Geometry of Resource Interaction — A Minimalist Approach.

Gray literature

  1. David R. Sherratt and Marco Solieri, Towards Atomic Graphs.
  2. Stefano Guerrini and Marco Solieri, Is the Optimal Implementation Inefficient? Elementary not.
  3. Marco Solieri, Sharing, Superposition and Expansion: Geometrical Studies on the Semantics and Implementation of λ-calculi and Proof-nets.
  4. Stefano Guerrini, Thomas Leventis, Marco Solieri, Deep into Optimality — Complexity and correctness of sharing implementation of bounded logic.
  5. Marco Solieri, Ottimalità dell'ottimalità — Complessità della riduzione su grafi di condivisione.