We study the semantics of an untyped λ-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 an operational semantics and a type assignment system of intersection types, and prove that types are invariant under reduction and expansion of term and state configurations, and characterize convergent terms via their typings.

Intersection types for a λ-calculus with global store

de'Liguoro, Ugo
;
Treglia, Riccardo
2021-01-01

Abstract

We study the semantics of an untyped λ-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 an operational semantics and a type assignment system of intersection types, and prove that types are invariant under reduction and expansion of term and state configurations, and characterize convergent terms via their typings.
2021
Principles and Practice of Declarative Programming - PPDP 2021
Tallin
6-8 Settembre 2021
PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming
Association for Computing Machinery
1
11
9781450386890
https://dl.acm.org/doi/10.1145/3479394.3479400
Theory of computation Lambda calculus Type theory Operational semantics
de'Liguoro, Ugo; Treglia, Riccardo
File in questo prodotto:
File Dimensione Formato  
PPDP21-Draft.pdf

Accesso riservato

Tipo di file: PREPRINT (PRIMA BOZZA)
Dimensione 517.47 kB
Formato Adobe PDF
517.47 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/1814740
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? ND
social impact