In this paper, we present Λt∧, a fully typed λ-calculus based on the intersection-type system discipline, which is a counterpart à la Church of the type assignment system as invented by Coppo and Dezani. The relationship between Λt∧ and the intersection type assignment system is the standard isomorphism between typed and type assignment system, and so the typed language inherits from the untyped system all the good properties, like subject reduction and strong normalization. Moreover both type checking and type reconstruction are decidable.

Intersection Types a la Church

RONCHI DELLA ROCCA, Simonetta
2007-01-01

Abstract

In this paper, we present Λt∧, a fully typed λ-calculus based on the intersection-type system discipline, which is a counterpart à la Church of the type assignment system as invented by Coppo and Dezani. The relationship between Λt∧ and the intersection type assignment system is the standard isomorphism between typed and type assignment system, and so the typed language inherits from the untyped system all the good properties, like subject reduction and strong normalization. Moreover both type checking and type reconstruction are decidable.
2007
205(9)
1371
1386
http://www.di.unito.it/~ronchi/
Logics and Intersection-Types; λ-calculus à la Curry and à la Church
L. LIQUORI; S. RONCHI DELLA ROCCA
File in questo prodotto:
File Dimensione Formato  
InfComp.pdf

Accesso riservato

Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 723.01 kB
Formato Adobe PDF
723.01 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: https://hdl.handle.net/2318/36750
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact