Categorical data types in parametric polymorphism
- 4 March 1994
- journal article
- research article
- Published by Cambridge University Press (CUP) in Mathematical Structures in Computer Science
- Vol. 4 (1) , 71-109
- https://doi.org/10.1017/s0960129500000372
Abstract
The categorical data types in models of second order lambda calculus are studied. We prove that Reynolds parametricity is a sufficient and necessary condition for the categorical data types to fulfill the universal properties.Keywords
This publication has 25 references indexed in Scilit:
- A note on categorical datatypesPublished by Springer Nature ,2005
- Inductively defined types in the Calculus of ConstructionsPublished by Springer Nature ,1990
- Extensional models for polymorphismTheoretical Computer Science, 1988
- Categorical semantics for higher order polymorphic lambda calculusThe Journal of Symbolic Logic, 1987
- The system F of variable types, fifteen years laterTheoretical Computer Science, 1986
- The Expressiveness of Simple and Second-Order Type StructuresJournal of the ACM, 1983
- Algebraic specification of data types: A synthetic approachTheory of Computing Systems, 1981
- Sheaves and logicPublished by Springer Nature ,1979
- A fixpoint theorem for complete categoriesMathematische Zeitschrift, 1968
- A lattice-theoretical fixpoint theorem and its applicationsPacific Journal of Mathematics, 1955