BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Type Refinement in the Abstract - Noam Zeilberger\, MSR-INRIA
DTSTART:20131016T140000Z
DTEND:20131016T150000Z
UID:TALK48397@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:The concept of refinement in type theory is a way of reconcili
 ng the "intrinsic" and the "extrinsic" meanings of types (aka "types à la
  Church" and "types à la Curry"). In a recent paper with Paul-André Mell
 iès[1]\, we looked at this idea more carefully and settled on the simple 
 conclusion that the type-theoretic notion of "type refinement system" may 
 be identified with the category-theoretic notion of "functor". This genera
 lization of the traditional analogy (type system ~ category) has the pract
 ical benefit\, we believe\, of bringing the interests of type theory and t
 he tools of categorical logic much closer together. For example\, workaday
  concepts such as "typing judgments"\, "subtyping"\, and "typing derivatio
 ns" can be analyzed mathematically on general terms\, without having to fi
 x a particular formal system. In the paper\, we also use this corresponden
 ce to motivate the study of "monoidal closed bifibrations"\, which is esse
 ntially the type theory induced by combining the usual product and functio
 n spaces with inverse image and direct image type constructors. We have fo
 und that many interesting new phenomena arise by this simple twist on the 
 simply-typed lambda calculus.\n\nIn the talk I will try to motivate and ex
 plain these ideas from a relatively elementary perspective (some backgroun
 d in both type theory and\ncategorical logic could be helpful\, but *eithe
 r* should be sufficient).\n\n[1]"Type refinement and monoidal closed bifib
 rations"\, http://arxiv.org/abs/1310.0263\n\n
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR