Sciweavers

Share
APAL
2007

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

8 years 3 months ago
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...
Fairouz Kamareddine, Karim Nour
Added 08 Dec 2010
Updated 08 Dec 2010
Type Journal
Year 2007
Where APAL
Authors Fairouz Kamareddine, Karim Nour
Comments (0)
books