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

In this paper we consider a type system with a universal type ω where any term (whether open or closed, β-normalising or not) has type ω. We provide this type system with a realisability semantics where an atomic type is interpreted as the set of λ-terms saturated by a certain relation. The variation of the saturation relation gives a number of interpretations to each type. We show the soundness and completeness of our semantics and that for different notions of saturation (based on weak head reduction and normal β-reduction) we obtain the same interpretation for types. Since the presence of ω prevents typability and realisability from coinciding and creates extra difficulties in characterizing the interpretation of a type, we define a class U+ of the so-called positive types (where ω can only occur at specific positions). We show that if a term inhabits a positive type, then this term is β-normalisable and reduces to a closed term. In other words, positive types can be use...

• Type: Journal
• Year: 2007
• Where: APAL
• Authors: Fairouz Kamareddine, Karim Nour
• Keywords: APAL 2007, Atomic Type, Positive Types, Universal Type