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 listsAlgebra Reading Group on Sporadic Groups Particle Physics Seminars Cold Atoms## Other talksAccurate and efficient numerical methods for molecular dynamics and data science using adaptive thermostats Verification of Byzantine Fault Tolerant Systems Operator Preconditioning and Some Recent Developments for Boundary Integral Equations Intriguing Properties of Adversarial ML Attacks in the Problem Space School Seminar EV Charging Security at the Physical-Layer |