A Categorical Perspective on Type Refinement Systems

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

• Noam Zeilberger (University of Birmingham)
• Thursday 08 December 2016, 12:00-13:00
• CS 217.

If you have a question about this talk, please contact Uday Reddy.

A “type refinement system” is a type system built on top of a typed programming language, as an extra layer of typing. Type refinement systems in this sense have become increasingly popular in recent years as a lightweight mechanism for improving the correctness of programs. In this hopefully interactive talk, I will give an introduction to a categorical perspective on type refinement systems that I have been developing over several years in collaboration with Paul-André Melliès, based on the idea that any functor can be interpreted as an abstract type refinement system. Some questions to consider from this perspective include:

• What does it mean for a program to have more than one type?

• What is the meaning of the so-called “subsumption rule” (a classical typing rule found in systems with subtyping)?

• In what sense is Hoare logic a type refinement system?

• If type refinement systems are functors, what does it mean for a type refinement system to be a Grothendieck (bi)fibration?

Depending on available time and the interests of the audience, I will also give some examples illustrating how one can take advantage of the rich logical structure coming from a type refinement system that is simultaneously a monoidal closed functor and a bifibration.

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• CS 217
• Lab Lunch

Note that ex-directory lists are not shown.