University of Cambridge > > Microsoft Research Cambridge, public talks > Type Refinement in the Abstract

Type Refinement in the Abstract

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

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 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ès1, 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",

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

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity