A novel typed λ-calculus a` la Church with intersection types is proposed. The novelty is the presence of three type constructors representing different roles of the standard intersection type constructor. The main properties are Subject Reduction and the characterisation of typed λ-terms reducing to head normal forms.
YACC: Yet Another Church Calculus
Dezani-Ciancaglini, Mariangiola;de'Liguoro, Ugo;
2024-01-01
Abstract
A novel typed λ-calculus a` la Church with intersection types is proposed. The novelty is the presence of three type constructors representing different roles of the standard intersection type constructor. The main properties are Subject Reduction and the characterisation of typed λ-terms reducing to head normal forms.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
bdlv.pdf
Accesso riservato
Tipo di file:
POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione
423.42 kB
Formato
Adobe PDF
|
423.42 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.
