COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > A categorical perspective on type refinement systems

## A categorical perspective on type refinement systemsAdd 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
- Computer Laboratory talks
- Computing and Mathematics
- 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. |
## Other listsSCAMPS 09 - One day Symposium Life Science Centre for Family Research 2011 Archive## Other talksMOVED TO 28 JUNE 2018 It takes two to tango:platelet collagen receptor GPVI-dimer in thrombosis and clinical implications Far-infrared emission from AGN and why this changes everything Oncological imaging: introduction and non-radionuclide techniques Yikes! Why did past-me say he'd give a talk on future discounting? Cosmological Probes of Light Relics |