ACM/IEEE Symposium on Logic in Computer Science

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

Tenth Annual IEEE Symposium on

Logic in Computer Science (LICS 1995)

Paper: A logic of subtyping (at LICS 1995)

Authors: Giuseppe Longo Kathleen Milsted Sergei 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 = 	 {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}

Last modified: 2022-10-3113:49
Sam Staton