University of Birmingham > Talks@bham > Lab Lunch > 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)
- 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:Note that ex-directory lists are not shown. |
## Other listsApplied Mathematics Seminar Series Lab Lunch Dinner Table Terrorism - Achieving Food Security## Other talksBases for permutation groups TBA TBA Kneser Graphs are Hamiltonian Integral equation methods for acoustic scattering by fractals TBA |