A categorical perspective on type refinement systems

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

• Noam Zeilberger, University of Birmingham
• Friday 09 December 2016, 14:00-15:00
• FW26.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.