Ugo de'Liguoro ; Riccardo Treglia - Intersection Types for a Computational Lambda-Calculus with Global State

fi:10010 - Fundamenta Informaticae, August 29, 2025, Volume 194, Issue 3 - https://doi.org/10.46298/fi.10010
Intersection Types for a Computational Lambda-Calculus with Global StateArticle

Authors: Ugo de'Liguoro ; Riccardo Treglia

    We study the semantics of an untyped lambda-calculus equipped with operators representing read and write operations from and to a global store. We adopt the monadic approach to model side-effects and treat read and write as algebraic operations over a monad. We introduce operational and denotational semantics and a type assignment system of intersection types and prove that types are invariant under the reduction and expansion of term and state configurations. Finally, we characterize convergent terms via their typings.


    Volume: Volume 194, Issue 3
    Published on: August 29, 2025
    Accepted on: May 20, 2025
    Submitted on: September 7, 2022
    Keywords: Logic in Computer Science, Programming Languages, F.3.2; F.4.1