Abstract:

The concept of "refinement" in type theory is a way of reconciling the "intrinsic" and the "extrinsic" semantics of types (a.k.a. "Church and Curry", cf. http://www.cs.cmu.edu/~fp/papers/andrews08.pdf).  I will begin by giving a rigorous analysis of this concept, and explain how it leads to a natural, equivalent reformulation of Grothendieck's definition of "bifibration".  Then I will try to motivate the study of "monoidal closed bifibrations", as a logical abstraction modelling many common situations in proof theory and programming.  One example I am particularly interested in is the sort of "polymorphic double-negation" appearing in Filinski's work on monadic reflection, and I will describe how the language of monoidal closed bifibrations can be used to explain elements of this idea.

About Noam Zeilberger