Parametricity and Dependent Types

Bernardy, J-P., Jansson, P. & Paterson, R. A. (2010). Parametricity and Dependent Types. Paper presented at the International Conference on Functional Programming, 27-09-2010 - 29-09-2010, Baltimore, USA.

[img]
Preview
Text - Accepted Version
Download (362kB) | Preview

Abstract

Reynolds' abstraction theorem shows how a typing judgement in System F can be translated into a relational statement (in second order predicate logic) about inhabitants of the type. We (in second order predicate logic) about inhabitants of the type. We obtain a similar result for a single lambda calculus (a pure type system), in which terms, types and their relations are expressed. Working within a single system dispenses with the need for an interpretation layer, allowing for an unusually simple presentation. While the unification puts some constraints on the type system (which we spell out), the result applies to many interesting cases, including dependently-typed ones.

Item Type: Conference or Workshop Item (Paper)
Additional Information: © Paterson, R | ACM 2010. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in ICFP '10 Proceedings of the 15th ACM SIGPLAN international conference on Functional programming, http://dx.doi.org/10.1145/1863543.1863592
Uncontrolled Keywords: Pure type system, Abstraction theorem, Free theorems
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Divisions: School of Informatics > Department of Computing
URI: http://openaccess.city.ac.uk/id/eprint/13223

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year

View more statistics