Parametricity and dependent types

' 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 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. Categories and Subject Descriptors F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs--Type Structure General Terms Languages, Theory Pure type system, Abstraction theorem, Free theorems

• Type: Conference
• Year: 2010
• Where: ICFP
• Authors: Jean-Philippe Bernardy, Patrik Jansson, Ross Paterson
• Keywords: Abstraction Theorem, ICFP 2010, Programming Languages, Pure Type System, Type System