BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A categorical perspective on type refinement systems - Noam Zeilbe
 rger\, University of Birmingham
DTSTART:20161209T140000Z
DTEND:20161209T150000Z
UID:TALK68794@talks.cam.ac.uk
CONTACT:Dominic Mulligan
DESCRIPTION:A "type refinement system" is a type system built on top of a 
 typed\nprogramming language\, as an extra layer of typing. Type refinement
 \nsystems in this sense have become increasingly popular in recent years\n
 as a lightweight mechanism for improving the correctness of programs.\nIn 
 the talk\, I will give an introduction to a categorical perspective\non ty
 pe refinement systems that I have been developing over several\nyears in c
 ollaboration with Paul-André Melliès\, based on the simple\nidea of mode
 lling a type refinement system as an "erasure" functor\nfrom a category of
  typing derivations to a category of terms.  Some\nquestions one can consi
 der from this perspective include:\n\n* What does it mean for a program to
  have more than one type? What does it\n  mean for a typing judgment to ha
 ve more than one derivation?\n\n* How should we understand the so-called "
 subsumption rule" (a classical\n  typing rule found in systems with subtyp
 ing)?\n\n* If functors are type refinement systems\, what does it mean for
  a\n  functor to be a Grothendieck (bi)fibration?\n\nA particular class of
  type refinement systems that are especially\nnatural from this perspectiv
 e are ones coming from a strict monoidal\nclosed functor that is simultane
 ously a bifibration. I will give some\nexamples illustrating how such type
  refinement systems can be used\nto give an axiomatic account of some phen
 omena from the semantics of\nseparation logic and lambda calculus.
LOCATION:FW26
END:VEVENT
END:VCALENDAR