Name
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 existential types, inductive types, coinductive types and general recursive types. We show that the recursive types satisfy a universal property called dinaturality, and we develop reasoning principles for the constructed types. In the case of recursive types, the reasoning principle is a mixed induction/coinduction principle, with the curious property that coinduction holds for general relations, but induction only for a limited collection of "admissible" relations. A similar property was observed in Pitts' 1995 analysis of recursive types in domain theory. In a future paper we will develop a category theoretic notion of models of the logic presented here, and show how the results developed in the logic can be transferred to the models. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.2168/LMCS-2(5:2)2006 | LOGICAL METHODS IN COMPUTER SCIENCE |
Keywords | Field | DocType |
parametric polymorphism,domain theory,recursive types | Discrete mathematics,Computer science,Domain theory,Type theory,Coinduction,Universal property,Fixed point,Parametricity,Recursion | Journal |
Volume | Issue | ISSN |
2 | 5 | 1860-5974 |
Citations | PageRank | References |
5 | 0.47 | 14 |
Authors | ||
4 | ||
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 |
| Benjamin Pierce | 4 | 5 | 0.47 |