BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Models of Polymorphism - Sean Moss (DPMMS)
DTSTART:20150423T130000Z
DTEND:20150423T140000Z
UID:TALK59257@talks.cam.ac.uk
CONTACT:Sean Moss
DESCRIPTION:System F\, or the second-order typed λ-calculus\, is a versio
 n of type theory with polymorphic types. For example\, there is a polymorp
 hic type of lists in X\, where X varies over all types. A fibration captur
 es the notion of a category whose objects are families indexed by the obje
 cts of another and thus lends itself to a semantics for System F. In fact\
 , there is a complete class of fibrational models for System F which arise
  from toposes considered as intuitionistic universes of sets.
LOCATION:CMS\, MR13
END:VEVENT
END:VCALENDAR