Name
Title | ||
|---|---|---|
Parametric Domain-theoretic Models of Polymorphic Intuitionistic / Linear Lambda Calculus |
Abstract | ||
|---|---|---|
We present a formalization of a version of Abadi and Plotkin's logic for parametricity for a polymorphic dual intuitionistic / linear type theory with fixed points, and show, following Plotkin's suggestions, that it can be used to define a wide collection of types, including solutions to recursive domain equations. We further define a notion of parametric LAPL-structure and prove that it provides a sound and complete class of models for the logic, and conclude that such models have solutions for a wide class of recursive domain equations. Finally, we present a concrete parametric LAPL-structure based on suitable categories of partial equivalence relations over a universal model of the untyped lambda calculus. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1016/j.entcs.2005.11.057 | Electronic Notes in Theoretical Computer Science (ENTCS) |
Keywords | DocType | Volume |
parametric polymorphism,fixed point,type theory,lambda calculus,domain theory,polymorphism,equivalence relation | Journal | 155, |
ISSN | Citations | PageRank |
1571-0661 | 4 | 0.43 |
References | Authors | |
13 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Lars Birkedal | 1 | 1481 | 96.84 |
| Rasmus Ejlers Møgelberg | 2 | 204 | 16.63 |
| Rasmus Lerchedahl Petersen | 3 | 110 | 6.64 |