| 1. |
|
|
| 2. |
- Bernardy, Jean-Philippe, 1978, et al.
(författare)
-
Parametricity and Dependent Types
- 2010
-
Ingår i: SIGPLAN Notices (ACM Special Interest Group on Programming Languages). - : Association for Computing Machinery (ACM). - 0730-8566 .- 0362-1340 .- 1558-1160. ; 45:9, s. 345-356
-
Tidskriftsartikel (refereegranskat)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.
|
|
| 3. |
- Bernardy, Jean-Philippe, 1978, et al.
(författare)
-
Parametricity and dependent types
- 2010
-
Ingår i: International Conference on Functional Programming, September 27-29, 2010, Baltimore, Maryland.
-
Konferensbidrag (refereegranskat)abstract
- Reynolds' abstraction theorem shows how a typingjudgement in System F can be translated into a relational statement (in second order predicate logic)about inhabitants of the type. We expose a similar result, whereterms, types, and their relations are expressed in a single typed lambda calculus (a pure type system).Working within a single system dispenses the need for aninterpretation layer, allowing for an unusually simplepresentation. While the unification puts some constraints on the type system(which we spell out), the result applies to many interesting cases, includingdependently-typed ones.
|
|
| 4. |
- Bernardy, Jean-Philippe, 1978, et al.
(författare)
-
Proofs for Free - Parametricity for dependent types
- 2012
-
Ingår i: Journal of Functional Programming. - 1469-7653 .- 0956-7968. ; 22:2, s. 107-152
-
Tidskriftsartikel (refereegranskat)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 obtain a similar result for pure type systems: for any PTS used as a programming language, there is a PTS that can be used as a logic for parametricity. Types in the source PTS are translated to relations (expressed as types) in the target. Similarly, values of a given type are translated to proofs that the values satisfy the relational interpretation. We extend the result to inductive families.We also show that the assumption that every term satisfies the parametricity condition generated by its type is consistent with the generated logic. Our proof gives a computationally meaningful way to interpret that assumption.
|
|
