University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > 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 Dominic Mulligan.

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 the 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 simple idea of modelling a type refinement system as an “erasure” functor from a category of typing derivations to a category of terms. Some questions one can consider from this perspective include:

  • What does it mean for a program to have more than one type? What does it mean for a typing judgment to have more than one derivation?
  • How should we understand the so-called “subsumption rule” (a classical typing rule found in systems with subtyping)?
  • If functors are type refinement systems, what does it mean for a functor to be a Grothendieck (bi)fibration?

A particular class of type refinement systems that are especially natural from this perspective are ones coming from a strict monoidal closed functor that is simultaneously a bifibration. I will give some examples illustrating how such type refinement systems can be used to give an axiomatic account of some phenomena from the semantics of separation logic and lambda calculus.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2020 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity