The core of this paper is a new proposal for a true intersection typed lambda calculus, without any meta-level notion. Namely, any typable term (in the intersection type inference) has a corresponding typed term (which is the same as the untyped term by erasing the type decorations and the typed term constructors) with the same type, and vice versa. The main idea is to introduce a relevant parallel term constructor which corresponds to the intersection type constructor, in such a way that terms in parallel share the same resources, that is, the same context of free typed variables.

A typed lambda calculus with intersection types

BONO, Viviana;VENNERI, Battistina;BETTINI, LORENZO
2008

Abstract

The core of this paper is a new proposal for a true intersection typed lambda calculus, without any meta-level notion. Namely, any typable term (in the intersection type inference) has a corresponding typed term (which is the same as the untyped term by erasing the type decorations and the typed term constructors) with the same type, and vice versa. The main idea is to introduce a relevant parallel term constructor which corresponds to the intersection type constructor, in such a way that terms in parallel share the same resources, that is, the same context of free typed variables.
398
1-3
95
113
V. BONO; B. VENNERI; L. BETTINI
File in questo prodotto:
File Dimensione Formato  
intersection.pdf

Accesso riservato

Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 191.21 kB
Formato Adobe PDF
191.21 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.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/2318/29094
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 12
  • ???jsp.display-item.citation.isi??? 7
social impact