COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Comprehensive Parametric Polymorphism

## Comprehensive Parametric PolymorphismAdd to your list(s) Download to your calendar using vCal - Fredrik Nordvall Forsberg, Mathematically Structured Programming Group at the University of Strathclyde
- Friday 11 March 2016, 14:00-15:00
- FW26.
If you have a question about this talk, please contact Ohad Kammar. In this talk, we explore the fundamental category-theoretic structure needed to model relational parametricity (i.e., the fact that polymorphic programs preserve all relations) for the polymorphic lambda calculus (a.k.a. System F). Taken separately, the notions of categorical model of impredicative polymorphism and relational parametricity are well-known (lambda2-fibrations and reflexive graph categories, respectively). Perhaps surprisingly, simply combining these two structures results in a notion that only enjoys the expected properties in case the underlying category is well-pointed. This rules out many categories of interest (e.g. functor categories) in the semantics of programming languages. To circumvent this restriction, we modify the definition of fibrational model of impredicative polymorphism by adding one further ingredient to the structure: comprehension in the sense of Lawvere. Our main result is that such comprehensive models, once further endowed with reflexive-graph-category structure, enjoy the expected consequences of parametricity. This is proved using a type-theoretic presentation of the category-theoretic structure, within which the desired consequences of parametricity are derived. Working in this type theory requires new techniques, since equality relations are not available, so that standard arguments that exploit equality need to be reworked. This is joint work with Neil Ghani and Alex Simpson. This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Computer Laboratory talks
- Computing and Mathematics
- FW26
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsImagers Interest Group The Centre For Financial Analysis & Policy Meeting the Challenge of Healthy Ageing in the 21st Century## Other talksMissing friars: rethinking late medieval medicine Equations in groups What has Engineering Design to say about Healthcare Improvement? Part IIB Poster Presentations A sex-linked supergene controls sperm morphology and swimming speed in a songbird TODAY Foster Talk - Localised RNA-based mechanisms underlie neuronal wiring |