Paper: System ST \beta-reduction and completeness (at LICS 2003)

Authors: Christophe Raffalli

Abstract

We prove that system ST (introduced in a previous work) enjoys subject reduction and is complete for realizability semantics. As far as the author knows, this is the only type system enjoying the second property. System ST is a very expressive type system, whose principle is to use two kinds of formulae: types (formulae with algorithmic content) and propositions (formulae without algorithmic content). The fact that subtyping is used to build propositions and that propositions can be used in types trough a special implication gives its great expressive power to the system: all the operators you can imagine are definable (union, intersection, singleton,...).

BibTeX

  @InProceedings{Raffalli-SystemSTbetareducti,
    author = 	 {Christophe Raffalli},
    title = 	 {System ST \beta-reduction and completeness},
    booktitle =  {Proceedings of the Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2003)},
    year =	 {2003},
    month =	 {June}, 
    pages =      {21--31},
    location =   {Ottawa, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }