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

Research output: Contribution to journalArticle

Abstract

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 used to represent abstract data types. The completeness theorem for 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 U+. We give a number of examples to explain the intuition behind the definition of U+ and to show that this class cannot be extended while keeping its desired properties. © 2007 Elsevier B.V. All rights reserved.

Original languageEnglish
Pages (from-to)180-198
Number of pages19
JournalAnnals of Pure and Applied Logic
Volume146
Issue number2-3
DOIs
Publication statusPublished - May 2007

Fingerprint

Type Systems
Completeness
Intersection
Term
Saturation
Abstract Data Types
Closed
Soundness
Semantics
Equivalence
Theorem
Interpretation

Keywords

  • Completeness
  • Intersection type systems
  • Normalisation
  • Positive types
  • Realisability semantics
  • Soundness
  • Subject expansion
  • Subject reduction

Cite this

@article{920bff2190184b03a404f80f4240d754,
title = "A completeness result for a realisability semantics for an intersection type system",
abstract = "In this paper we consider a type system with a universal type ? where any term (whether open or closed, {\ss}-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 {\ss}-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 {\ss}-normalisable and reduces to a closed term. In other words, positive types can be used to represent abstract data types. The completeness theorem for 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 U+. We give a number of examples to explain the intuition behind the definition of U+ and to show that this class cannot be extended while keeping its desired properties. {\circledC} 2007 Elsevier B.V. All rights reserved.",
keywords = "Completeness, Intersection type systems, Normalisation, Positive types, Realisability semantics, Soundness, Subject expansion, Subject reduction",
author = "Fairouz Kamareddine and Karim Nour",
year = "2007",
month = "5",
doi = "10.1016/j.apal.2007.02.001",
language = "English",
volume = "146",
pages = "180--198",
journal = "Annals of Pure and Applied Logic",
issn = "0168-0072",
publisher = "Elsevier",
number = "2-3",

}

A completeness result for a realisability semantics for an intersection type system. / Kamareddine, Fairouz; Nour, Karim.

In: Annals of Pure and Applied Logic, Vol. 146, No. 2-3, 05.2007, p. 180-198.

Research output: Contribution to journalArticle

TY - JOUR

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

AU - Kamareddine, Fairouz

AU - Nour, Karim

PY - 2007/5

Y1 - 2007/5

N2 - 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 used to represent abstract data types. The completeness theorem for 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 U+. We give a number of examples to explain the intuition behind the definition of U+ and to show that this class cannot be extended while keeping its desired properties. © 2007 Elsevier B.V. All rights reserved.

AB - 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 used to represent abstract data types. The completeness theorem for 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 U+. We give a number of examples to explain the intuition behind the definition of U+ and to show that this class cannot be extended while keeping its desired properties. © 2007 Elsevier B.V. All rights reserved.

KW - Completeness

KW - Intersection type systems

KW - Normalisation

KW - Positive types

KW - Realisability semantics

KW - Soundness

KW - Subject expansion

KW - Subject reduction

UR - http://www.scopus.com/inward/record.url?scp=34247150303&partnerID=8YFLogxK

U2 - 10.1016/j.apal.2007.02.001

DO - 10.1016/j.apal.2007.02.001

M3 - Article

VL - 146

SP - 180

EP - 198

JO - Annals of Pure and Applied Logic

JF - Annals of Pure and Applied Logic

SN - 0168-0072

IS - 2-3

ER -