Conference and Journal Papers:

• Lorenzo Gheri and Nobuko Yoshida: Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection. OOPSLA 2023 : to appear. Extended version available as a preprint.

• Lorenzo Gheri, Ivan Lanese, Neil Sayers, Emilio Tuosto, and Nobuko Yoshida: Design-by-Contract for Flexible Multiparty Session Protocols. ECOOP 2022: 8:1-8:28. 

• David Castro-Perez, Francisco Ferreira, Lorenzo Gheri, and Nobuko Yoshida: Zooid: A DSL for Certified Multiparty Computation. PLDI 2021 : 237 - 251. 

• Nobuko Yoshida and Lorenzo Gheri. A Very Gentle Introduction to Multiparty Session Types. ICDCIT 2020 : 73 - 93. (Invited paper.)  

• Lorenzo Gheri and Andrei Popescu. A formalized general theory of syntax with bindings: Extended Version. In: J. Autom. Reasoning. (2020). Extended version of the ITP 2017 paper with the same name.

• Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, and Dmitriy Traytel. Bindings as Bounded Natural Functors. In Weirich, S. (ed.) 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019), ACM, 2019, Article 22, pp. 22:1–22:34. Isabelle/HOL scripts associated to the paper.

• Lorenzo Gheri and Andrei Popescu. A formalized general theory of syntax with bindings. In: ITP 2017. LNCS 10499, 241-261, Springer.

Formal Proof Developments and Artifacts:

• Lorenzo Gheri, Ivan Lanese, Neil Sayers, Emilio Tuosto, and Nobuko Yoshida. Design-by-Contract for Flexible Multiparty Session Protocols (Artifact). Dagstuhl Artifacts Ser. 8(2): 21:1-21:5 (2022)

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

Drafts:

• Lorenzo Gheri, Andrei Popescu. A Case Study in Reasoning about Syntax with Bindings: The Church-Rosser and Standardization Theorems.  In this paper, we instantiate our framework to the syntax of lambda-calculus and formalize the development leading to two main results: the Church-Rosser and Standardization theorems. Our work covers both the call-by-name and call-by-value versions of the calculus, following a classic paper by Gordon Plotkin. During the formalization, we were able to stay focused on the high-level ideas of the development, thanks to the arsenal provided by our general theory.

Phd Thesis:

• Lorenzo Gheri. PhD Thesis.