## 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. Møgelberg, R.L. Petersen, Parametric domain-theoretical models of polymorphic intuitionistic/linear lambda calculus, in: M. Escardó, A. Jung, M. Mislove (Eds.), Proceedings of Mathematical Foundations of Programming Semantics 2005, vol. 155, 2005, pp. 191–217; L. Birkedal, R.E. Møgelberg, 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.

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.

Original language | English |
---|---|

Journal | Theoretical Computer Science |

Volume | 388 |

Issue number | 1-3 |

Pages (from-to) | 152-172 |

ISSN | 0304-3975 |

DOIs | |

Publication status | Published - 2010 |

## Keywords

- Parametric polymorphism
- Domain theory
- Realizability models