A completeness result for a realisability semantics for an intersection type system

Fairouz Kamareddine, Karim Nour

In this paper we consider a type system with a universal type $\omega$ where any term (whether open or closed, $\beta$-normalising or not) has type $\omega$. We provide this type system with a r…