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.
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.
