Name
Abstract | ||
|---|---|---|
In a recent article [L. Birkedal, R. E. Mogelberg, and R. L. Petersen. Parametric domain-theoretic models of linear Abadi & Plotkin logic. Technical Report TR-2005-57, IT University of Copenhagen, February 2005] the first two authors and R.L. Petersen have defined a notion of parametric LAPL-structure. Such structures are parametric models of the equational theory PILLY, a polymorphic intuitionistic / linear type theory with fixed points, in which one can reason using parametricity and, for example, solve a large class of domain equations [L. Birkedal, R. E. Mogelberg, and R. L. Petersen. Parametric domain-theoretic models of linear Abadi & Plotkin logic. Technical Report TR-2005-57, IT University of Copenhagen, February 2005, L Birkedal, R. E. Mogelberg, and R. L. Petersen. Parametric domain-theoretic models of polymorphic intuitionistic / linear lambda calculus. In Proceedings of the Twenty-first Conference on the Mathematical Foundations of Programming Semantics, 2005. To appear]. Based on recent work by Simpson and Rosolini [G. Rosolini and A. Simpson. Using synthetic domain theory to prove operational properties of a polymorphic programming language based on strictness. Manuscript, 2004] we construct a family of parametric LAPL-structures using synthetic domain theory and use the results of loc. cit. and results about LAPL-structures to prove operational consequences of parametricity for a strict version of the Lily programming language. In particular we can show that one can solve domain equations in the strict version of Lily up to ground contextual equivalence. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1016/j.entcs.2005.11.058 | Ann. Pure Appl. Logic |
Keywords | Field | DocType |
parametric polymorphism,parametric model,domain theory,polymorphism,type theory | Discrete mathematics,Algebra,Parametric polymorphism,Domain theory,Type theory,Equivalence (measure theory),Mathematical proof,Metalanguage,Parametricity,Recursion,Mathematics | Journal |
Volume | Issue | ISSN |
155, | 2 | Electronic Notes in Theoretical Computer Science |
Citations | PageRank | References |
4 | 0.45 | 17 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Rasmus Ejlers Møgelberg | 1 | 204 | 16.63 |
| Lars Birkedal | 2 | 1481 | 96.84 |
| Giuseppe Rosolini | 3 | 93 | 17.27 |