Talk: Noam Zeilberger - Type refinement and monoidal closed bifibrations
Oplysninger om arrangementet
Tidspunkt
Sted
5335-395 Nygaard Møderum
Arrangør
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.