University of Birmingham > Talks@bham > Theoretical computer science seminar > Deciding subtype entailment

Deciding subtype entailment

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Paul Taylor.

Type systems with subtyping have a long-standing reputation for being difficult to deal with, not least because the problem of entailment (determining whether one subtyping constraint implies another) has never been shown decidable.

In this talk, I’ll describe some work-in-progress arguing that this is an artifact of a particular definition of subtyping, rather than an inherent problem. By defining subtyping in a style reminiscent of Gentzen’s classical sequent calculus (with multiple types on the left and right of the subtyping symbol), we come up with a different subtyping relation which has the same basic subtyping rules as the standard definition, yet whose entailment relation is easily decided. Futhermore, the resulting structure is algebraically well-behaved, (thanks to the connection between sequent-like systems and distributive lattices drawn by Cederquist and Coquand), and seems like it would form a better basis for the design of type systems with subtyping than the standard approach.

This talk is part of the Theoretical computer science seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.