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

Research output: Contribution to journalArticle

8 Citations (Scopus)

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

Keywords

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

Fingerprint Dive into the research topics of 'A completeness result for a realisability semantics for an intersection type system'. Together they form a unique fingerprint.

  • Cite this