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:Microsoft Research Cambridge\, public talks
SUMMARY:Type Refinement in the Abstract - Noam Zeilberger\
, MSR-INRIA
DTSTART;TZID=Europe/London:20131016T150000
DTEND;TZID=Europe/London:20131016T160000
UID:TALK48397AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/48397
DESCRIPTION:The concept of refinement in type theory is a way
of reconciling the "intrinsic" and the "extrinsic"
meanings of types (aka "types à la Church" and "t
ypes à la Curry"). In a recent paper with Paul-And
ré Melliès[1]\, we looked at this idea more carefu
lly and settled on the simple conclusion that the
type-theoretic notion of "type refinement system"
may be identified with the category-theoretic noti
on of "functor". This generalization of the tradit
ional analogy (type system ~ category) has the pra
ctical benefit\, we believe\, of bringing the inte
rests of type theory and the tools of categorical
logic much closer together. For example\, workaday
concepts such as "typing judgments"\, "subtyping"
\, and "typing derivations" can be analyzed mathem
atically on general terms\, without having to fix
a particular formal system. In the paper\, we also
use this correspondence to motivate the study of
"monoidal closed bifibrations"\, which is essentia
lly the type theory induced by combining the usual
product and function spaces with inverse image an
d direct image type constructors. We have found th
at many interesting new phenomena arise by this si
mple twist on the simply-typed lambda calculus.\n\
nIn the talk I will try to motivate and explain th
ese ideas from a relatively elementary perspective
(some background in both type theory and\ncategor
ical logic could be helpful\, but *either* should
be sufficient).\n\n[1]"Type refinement and monoida
l closed bifibrations"\, http://arxiv.org/abs/1310
.0263\n\n
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station R
oad\, Cambridge\, CB1 2FB
CONTACT:Microsoft Research Cambridge Talks Admins
END:VEVENT
END:VCALENDAR