Type Refinement in the Abstract

Add to your list(s) Download to your calendar using vCal

• Noam Zeilberger, MSR-INRIA
• Wednesday 16 October 2013, 15:00-16:00
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

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 “types à la Curry”). In a recent paper with Paul-André Melliès¹, 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 generalization of the traditional analogy (type system ~ category) has the practical benefit, we believe, of bringing the interests 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 mathematically 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 essentially the type theory induced by combining the usual product and function spaces with inverse image and direct image type constructors. We have found that many interesting new phenomena arise by this simple twist on the simply-typed lambda calculus.

In the talk I will try to motivate and explain these ideas from a relatively elementary perspective (some background in both type theory and categorical logic could be helpful, but either should be sufficient).

refinement and monoidal closed bifibrations", http://arxiv.org/abs/1310.0263

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.