BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:Comprehensive Parametric Polymorphism - Fredrik No
rdvall Forsberg\, Mathematically Structured Progra
mming Group at the University of Strathclyde
DTSTART;TZID=Europe/London:20160311T140000
DTEND;TZID=Europe/London:20160311T150000
UID:TALK64146AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/64146
DESCRIPTION:In this talk\, we explore the fundamental category
-theoretic structure\nneeded to model relational p
arametricity (i.e.\, the fact that\npolymorphic pr
ograms preserve all relations) for the polymorphic
\nlambda calculus (a.k.a. System F). Taken separat
ely\, the notions of\ncategorical model of impredi
cative polymorphism and relational\nparametricity
are well-known (lambda2-fibrations and reflexive g
raph\ncategories\, respectively). Perhaps surprisi
ngly\, simply combining\nthese two structures resu
lts in a notion that only enjoys the expected\npro
perties in case the underlying category is well-po
inted. This rules\nout many categories of interest
(e.g. functor categories) in the\nsemantics of pr
ogramming languages.\n\nTo circumvent this restric
tion\, we modify the definition of\nfibrational mo
del of impredicative polymorphism by adding one fu
rther\ningredient to the structure: comprehension
in the sense of\nLawvere. Our main result is that
such comprehensive models\, once\nfurther endowed
with reflexive-graph-category structure\, enjoy th
e\nexpected consequences of parametricity. This is
proved using a\ntype-theoretic presentation of th
e category-theoretic structure\,\nwithin which the
desired consequences of parametricity are derived
.\nWorking in this type theory requires new techni
ques\, since equality\nrelations are not available
\, so that standard arguments that exploit\nequali
ty need to be reworked.\n\nThis is joint work with
Neil Ghani and Alex Simpson.
LOCATION:FW26
CONTACT:Ohad Kammar
END:VEVENT
END:VCALENDAR