Ph.D. Thesis
The computational core: reduction theory and intersection type discipline

Journal papers

Ugo de'Liguoro and T. - From semantics to types: The case of the imperative λ-calculus. Theoretical Computer Science 2023 [ link ]

Claudia Faggian, Giulio Guerrieri, Ugo de'Liguoro, and T. - On reduction and normalization in the computational core. MSCS 2023 [ pdf ]

Ugo de’Liguoro and T. - The untyped computational lambda-calculus and its intersection type discipline. Theoretical Computer Science 2020 [ link ]

Conference papers

Claudio Sacredoti Coen and T. - Properties of a Computational Lambda Calculus for Higher-Order Relational Queries. ICTCS 2023

Francesco Gavazzo, T., and Gabriele Vanoni - Monadic Intersection Types. TYPES 2023 [ pdf ]

Ugo de'Liguoro and T. - A filter model for the state monad. ICTCS 2021

Ugo de'Liguoro and T. - Intersection Types for a Computational lambda-Calculus with Global Store. PPDP 2021 [ pdf ]

Ugo de'Liguoro and T. - From semantics to types: the case of the imperative lambda-calculus. MFPS 2021 [ slides | Ugo's talk ]

Ugo de'Liguoro and T. - Intersection Types for a Computational lambda-Calculus with Global State. TYPES 2021 [ pdf ]

Ugo de’Liguoro and T. - Intersection Types for the Computational lambda-Calculus. ICTCS 2019 [ pdf ]

Workshop and Congress presentations

T - The Dynamics of Filter Models. UMI Congress 23

Claudio Sacerdoti Coen and T. - Confluence of a Computational Lambda Calculus for Higher-Order Relational Queries. IWC 23

Ugo de'Liguoro and T. - The Characterization of Convergence in Computational Lambda-Calculi via Intersection Types.  AILA 2022

Claudia Faggian, Giulio Guerrieri, and T. - Computational calculus: bridging reduction and evaluation. HOPE 2021 [ slide | video ]

Claudia Faggian, Giulio Guerrieri, and T. - Evaluation in the computational calculus is non-confluent. IWC 2021 [ video | pdf ]

Claudia Faggian, Giulio Guerrieri, and T. - Evaluation and convergence in the computational calculus. TLLA 2021 [ pdf ]

Ugo de'Liguoro and T. - On the reduction of the type-free computational λ-calculus. IWC 2020

T.- We Need LOv abstract machine for call-by-need calculus, and its complexity. AILA 2017

Unpablished papers

Ugo de’Liguoro and T. - Intersection Types for a Computational Lambda-Calculus with Global State. [ pdf ]

Ugo de’Liguoro and T. - Intersection Types for the Computational lambda-Calculus. Extended paper. [ pdf ]