Name
Abstract | ||
|---|---|---|
We present a domain-theoretical model of parametric polymorphism based on admissible per's over a domain-theoretical model of the untyped lambda calculus. The model is shown to be a model of Abadi & Plotkin's logic for parametricity, by the construction of an LAPL-structure as defined by the authors in [L. Birkedal, R.E. Mogelberg, R.L. Petersen, Parametric domain-theoretical models of polymorphic intuitionistic/linear lambda calculus, in: M. Escardo, A. Jung, M. Mislove (Eds.), Proceedings of Mathematical Foundations of Programming Semantics 2005, vol. 155, 2005, pp. 191-217; L. Birkedal, R.E. Mogelberg, R.L. Petersen, Category theoretical models of linear Abadi & Plotkin logic, 2006 (submitted for publication)]. This construction gives formal proof of solutions to a large class of recursive domain equations, which we explicate. As an example of a computation in the model, we explicitly describe the natural numbers object obtained using parametricity. The theory of admissible per's can be considered a domain theory for (impredicative) polymorphism. By studying various categories of admissible and chain complete per's and their relations, we discover a picture very similar to that of domain theory. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1016/j.tcs.2007.06.016 | Theor. Comput. Sci. |
Keywords | DocType | Volume |
E. Mogelberg,domain theory,parametric domain-theoretical model,recursive domain equation,Domain-theoretical model,category theoretical model,Domain theory,L. Birkedal,M. Mislove,R.L. Petersen,domain-theoretical model,Realizability models,Parametric polymorphism,parametric polymorphism,M. Escardo | Journal | 388 |
Issue | ISSN | Citations |
1-3 | Theoretical Computer Science | 9 |
PageRank | References | Authors |
0.57 | 13 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| L. Birkedal | 1 | 88 | 4.45 |
| Rasmus Ejlers Møgelberg | 2 | 204 | 16.63 |
| R. L. Petersen | 3 | 9 | 0.57 |