Deciding subtype entailment

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

• Stephen Dolan (Computer Lab, University of Cambridge)
• Friday 16 June 2017, 11:00-12:00
• Computer Science, The Sloman Lounge (UG).

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.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Computer Science, The Sloman Lounge (UG)
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.