A completeness result for a realisability semantics for an intersection type system
| dc.creator | Kamareddine, Fairouz | |
| dc.creator | Nour, Karim | |
| dc.date | 2009-05-04 | |
| dc.date.accessioned | 2026-07-07T13:11:24Z | |
| dc.date.available | 2026-07-07T13:11:24Z | |
| dc.description | 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 ${\mathbb 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 used to represent abstract data types. The completeness theorem for ${\mathbb U}^+$ becomes interesting indeed since it establishes a perfect equivalence between typable terms and terms that inhabit a type. In other words, typability and realisability coincide on ${\mathbb U}^+$. We give a number of examples to explain the intuition behind the definition of ${\mathbb U}^+$ and to show that this class cannot be extended while keeping its desired properties. | |
| dc.identifier | https://arxiv.org/abs/0905.0354 | |
| dc.identifier | http://arxiv.org/abs/0905.0354 | |
| dc.identifier | Annals of Pure and Applied Logic 146 (2007) 180-198 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/229276 | |
| dc.subject | Logic | |
| dc.title | A completeness result for a realisability semantics for an intersection type system | |
| dc.type | text |