A novel typed λ-calculus à 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
Barbanera, Franco;
2024-01-01
Abstract
A novel typed λ-calculus à 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:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
