University of Cambridge > > Junior Category Theory Seminar > Models of Polymorphism

Models of Polymorphism

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

If you have a question about this talk, please contact Sean Moss.

System F, or the second-order typed λ-calculus, is a version of type theory with polymorphic types. For example, there is a polymorphic type of lists in X, where X varies over all types. A fibration captures the notion of a category whose objects are families indexed by the objects of another and thus lends itself to a semantics for System F. In fact, there is a complete class of fibrational models for System F which arise from toposes considered as intuitionistic universes of sets.

This talk is part of the Junior Category Theory Seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


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