YACC: Yet Another Church Calculus
摘要
A novel typed \(\lambda \) -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 \(\lambda \) -terms reducing to head normal forms.