University of Birmingham > Talks@bham > Lab Lunch > A Categorical Perspective on Type Refinement Systems

A Categorical Perspective on Type Refinement Systems

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

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.

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.