CINECA IRIS Institutional Research Information System
IRIS è il sistema di gestione integrata dei dati della ricerca (persone, progetti, pubblicazioni, attività) adottato dall'Università degli Studi di Torino.
AperTO è l'archivio istituzionale Open Access destinato a raccogliere, rendere visibile e conservare la produzione scientifica dell'Università degli Studi di Torino.
EnglishWe propose an intersection type system for an imperative lambda-calculus based on a state monad and equipped with algebraic operations to read and write to the store. The system is derived by solving a suitable domain equation in the category of omega-algebraic lattices; the solution consists of a filter-model generalizing the well-known construction for ordinary lambda-calculus. Then the type system is obtained out of the term interpretations into the filter-model itself. The so obtained type system satisfies the ''type-semantics'' property, and it is sound and complete by construction.
| Titolo: | From Semantics to Types: the Case of the Imperative lambda-Calculus | |
| Autori Riconosciuti: | ||
| Autori: | Ugo de' Liguoro, Riccardo Treglia | |
| Data di pubblicazione: | 2021 | |
| Abstract: | We propose an intersection type system for an imperative lambda-calculus based on a state monad and equipped with algebraic operations to read and write to the store. The system is derived by solving a suitable domain equation in the category of omega-algebraic lattices; the solution consists of a filter-model generalizing the well-known construction for ordinary lambda-calculus. Then the type system is obtained out of the term interpretations into the filter-model itself. The so obtained type system satisfies the ''type-semantics'' property, and it is sound and complete by construction. | |
| Volume: | 351 | |
| Pagina iniziale: | 168 | |
| Pagina finale: | 183 | |
| Nome del convegno: | 37th Conference on Mathematical Foundations of Programming Semantics - MFPS 2021 | |
| Luogo del convegno: | Salzburg - Austria | |
| Anno del convegno: | 30 Agosto - 2 Settembre 2021 | |
| Digital Object Identifier (DOI): | 10.4204/EPTCS.351.11 | |
| Parole Chiave: | lambda calcolo, tipi, monadi | |
| Rivista: | ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | |
| Appare nelle tipologie: | 04B-Conference paper in rivista |
File in questo prodotto:
| File | Descrizione | Tipologia | Licenza | |
|---|---|---|---|---|
| MFPS2021.11.pdf | Articolo principale | PDF EDITORIALE | Open Access Visualizza/Apri |
Copyright © 2022