# Logic in Computer Science (LICS 2003)

## 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 Symp. on Logic in Computer Science, {LICS} 2003},
year =	 2003,
editor =	 {Phokion G. Kolaitis},
month =	 {June},
pages =      {21--},