We consider an untyped computational lambda calculus equipped with primitives to read and write from a global store. The calculus is modeled into a solution of a domain equation involving the state monad. We introduce an intersection type theory with subtyping such that the induced filter model is a solution of such an equation. Finally we define a type assignment system which is sound and complete w.r.t. any model of the calculus.
A Filter Model for the State Monad (short paper)
De'liguoro U.
;Treglia R.
2021-01-01
Abstract
We consider an untyped computational lambda calculus equipped with primitives to read and write from a global store. The calculus is modeled into a solution of a domain equation involving the state monad. We introduce an intersection type theory with subtyping such that the induced filter model is a solution of such an equation. Finally we define a type assignment system which is sound and complete w.r.t. any model of the calculus.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
de Liguoro, Treglia 2021 - A Filter Model for the State Monad (short paper).pdf
Accesso aperto
Tipo di file:
PDF EDITORIALE
Dimensione
545.81 kB
Formato
Adobe PDF
|
545.81 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
