BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Comprehensive Parametric Polymorphism - Fredrik Nordvall Forsberg\
 , Mathematically Structured Programming Group at the University of Strathc
 lyde
DTSTART:20160311T140000Z
DTEND:20160311T150000Z
UID:TALK64146@talks.cam.ac.uk
CONTACT:Ohad Kammar
DESCRIPTION:In this talk\, we explore the fundamental category-theoretic s
 tructure\nneeded to model relational parametricity (i.e.\, the fact that\n
 polymorphic programs preserve all relations) for the polymorphic\nlambda c
 alculus (a.k.a. System F). Taken separately\, the notions of\ncategorical 
 model of impredicative polymorphism and relational\nparametricity are well
 -known (lambda2-fibrations and reflexive graph\ncategories\, respectively)
 . Perhaps surprisingly\, simply combining\nthese two structures results in
  a notion that only enjoys the expected\nproperties in case the underlying
  category is well-pointed. This rules\nout many categories of interest (e.
 g. functor categories) in the\nsemantics of programming languages.\n\nTo c
 ircumvent this restriction\, we modify the definition of\nfibrational mode
 l of impredicative polymorphism by adding one further\ningredient to the s
 tructure: comprehension in the sense of\nLawvere. Our main result is that 
 such comprehensive models\, once\nfurther endowed with reflexive-graph-cat
 egory structure\, enjoy the\nexpected consequences of parametricity. This 
 is proved using a\ntype-theoretic presentation of the category-theoretic s
 tructure\,\nwithin which the desired consequences of parametricity are der
 ived.\nWorking in this type theory requires new techniques\, since equalit
 y\nrelations are not available\, so that standard arguments that exploit\n
 equality need to be reworked.\n\nThis is joint work with Neil Ghani and Al
 ex Simpson.
LOCATION:FW26
END:VEVENT
END:VCALENDAR