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:Junior Category Theory Seminar
SUMMARY:Models of Polymorphism - Sean Moss (DPMMS)
DTSTART;TZID=Europe/London:20150423T140000
DTEND;TZID=Europe/London:20150423T150000
UID:TALK59257AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/59257
DESCRIPTION:System F\, or the second-order typed λ-calculus\, 
 is a version of type theory with polymorphic types
 . For example\, there is a polymorphic type of lis
 ts in X\, where X varies over all types. A fibrati
 on captures the notion of a category whose objects
  are families indexed by the objects of another an
 d thus lends itself to a semantics for System F. I
 n fact\, there is a complete class of fibrational 
 models for System F which arise from toposes consi
 dered as intuitionistic universes of sets.
LOCATION:CMS\, MR13
CONTACT:Sean Moss
END:VEVENT
END:VCALENDAR