We study the logical semantics of an untyped λ-calculus equipped with operators representing read and write operations from and to a global store. Such a logic consists of an intersection type assignment system, which we derive from the denotational semantics of the calculus, based on the monadic approach to model computational λ-calculi.
From semantics to types: The case of the imperative λ-calculus
de'Liguoro, Ugo;Treglia, Riccardo
2023-01-01
Abstract
We study the logical semantics of an untyped λ-calculus equipped with operators representing read and write operations from and to a global store. Such a logic consists of an intersection type assignment system, which we derive from the denotational semantics of the calculus, based on the monadic approach to model computational λ-calculi.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
2023 dL Treglia - From semantics to types The case of the imperative λ-calculus.pdf
Accesso aperto
Tipo di file:
PDF EDITORIALE
Dimensione
526.72 kB
Formato
Adobe PDF
|
526.72 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
