Tenth Annual IEEE Symposium on

Logic in Computer Science (LICS 1995)

Paper: A logic of subtyping (at LICS 1995)

Authors: G. Loop K. Milsted S. Soloviev


The relation of inclusion between types has been suggested by the practice of programming, as it enriches the polymorphism of functional languages. We propose a simple (and linear) calculus of sequents for subtyping as logical entailment. This allows to derive a complete and coherent approach to subtyping from a few, logically meaningful, sequents. In particular, transitivity and anti-symmetry are derived from elementary logical principles, which stresses the power of sequents and Gentzen-style proof methods. Indeed, proof techniques based on cut-elimination are at the core of our results.


    author = 	 {G. Loop and K. Milsted and S. Soloviev},
    title = 	 {A logic of subtyping},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1995},
    year =	 1995,
    editor =	 {Dexter Kozen},
    month =	 {June}, 
    pages =      {292-299},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}