A completeness result for a realisability semantics for an intersection type system (Q882122)

The authors consider a type system with intersection types and a universal type \(\omega\) where any term has type \(\omega\). They provide this system with a realisability semantics where an atomic type is interpreted as a set of untyped \(\lambda\)-terms that is closed under a certain relation. The soundness and completeness for this semantics is obtained using a generalisation of the method due to \textit{J. R. Hindley} [``The simple semantics for Coppo-Dezani-Salle types'', Lect. Notes Comput. Sci. 137, 212--226 (1982; Zbl 0514.03009)]. Also, the authors find a set of types, called \({\mathbb U}^+\), for which typeabillity and realisability coincide.