ACM/IEEE Symposium on Logic in Computer Science

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

Eighteenth Annual IEEE Symposium on

Logic in Computer Science (LICS 2003)

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

Authors: Christophe Raffalli


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,...).


    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}

Last modified: 2021-11-1017:16
Sam Staton