Lics

ACM/IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Twentieth Annual IEEE Symposium on

Logic in Computer Science (LICS 2005)

Paper: Recursive Polymorphic Types and Parametricity in an Operational Framework (at LICS 2005)

Authors: Paul-André Melliès Jerome Vouillon

Abstract

We construct a realizability model of recursive polymorphic types, starting from an untyped language of terms and contexts. An orthogonality relation ? p indicates when a term e and a context p may be safely combined in the language. Types are interpreted as sets of terms closed by biorthogonality. Our main result states that recursive types are approximated by converging sequences of interval types. Our proof is based on a "type-directed" approximation technique, which departs from the "language-directed" approximation technique developed by MacQueen, Plotkin and Sethi in the ideal model. We thus keep the language elementary (a call-by-name ?-calculus) and unstratified (no typecase, no reduction labels). We also include a short account of parametricity, based on an orthogonality relation between quadruples of terms and contexts.

BibTeX

  @InProceedings{MellisVouillon-RecursivePolymorphi,
    author = 	 {Paul-André Melliès and Jerome Vouillon},
    title = 	 {Recursive Polymorphic Types and Parametricity in an Operational Framework},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005)},
    year =	 {2005},
    month =	 {June}, 
    pages =      {82--91},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2022-10-3113:49
Sam Staton