Paper: System ST \beta-reduction and completeness (at LICS 2003)
Authors: Christophe RaffalliAbstract
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--}, location = {Ottawa, Canada}, publisher = {IEEE Computer Society Press} }