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.

From Semantics to Types: the Case of the Imperative lambda-Calculus

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

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.
2021
37th Conference on Mathematical Foundations of Programming Semantics - MFPS 2021
Salzburg - Austria
30 Agosto - 2 Settembre 2021
351
168
183
lambda calcolo, tipi, monadi
Ugo de' Liguoro, Riccardo Treglia
File in questo prodotto:
File Dimensione Formato  
MFPS2021.11.pdf

Accesso aperto

Descrizione: Articolo principale
Tipo di file: PDF EDITORIALE
Dimensione 213.67 kB
Formato Adobe PDF
213.67 kB Adobe PDF Visualizza/Apri

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/1834653
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 0
social impact