Paper: A logic of subtyping (at LICS 1995)

Authors: Giuseppe Longo Kathleen Milsted Sergei Soloviev

Abstract

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.

BibTeX

  @InProceedings{LongoMilstedSolovie-Alogicofsubtyping,
    author = 	 {Giuseppe Longo and Kathleen Milsted and Sergei Soloviev},
    title = 	 {A logic of subtyping},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science (LICS 1995)},
    year =	 {1995},
    month =	 {June}, 
    pages =      {292--299},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }