CPO-models for second order lambda calculus with recursive types and subtyping
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 27 (1993) no. 3, pp. 221-260. 
@article{ITA_1993__27_3_221_0,
     author = {Poll, E. and Hemerik, C. and Ten Eikelder, H. M. M.},
     title = {CPO-models for second order lambda calculus with recursive types and subtyping},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {221--260},
     publisher = {EDP-Sciences},
     volume = {27},
     number = {3},
     year = {1993},
     mrnumber = {1227944},
     zbl = {0788.03016},
     language = {en},
     url = {http://archive.numdam.org/item/ITA_1993__27_3_221_0/}
}
TY  - JOUR
AU  - Poll, E.
AU  - Hemerik, C.
AU  - Ten Eikelder, H. M. M.
TI  - CPO-models for second order lambda calculus with recursive types and subtyping
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 1993
SP  - 221
EP  - 260
VL  - 27
IS  - 3
PB  - EDP-Sciences
UR  - http://archive.numdam.org/item/ITA_1993__27_3_221_0/
LA  - en
ID  - ITA_1993__27_3_221_0
ER  - 
%0 Journal Article
%A Poll, E.
%A Hemerik, C.
%A Ten Eikelder, H. M. M.
%T CPO-models for second order lambda calculus with recursive types and subtyping
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 1993
%P 221-260
%V 27
%N 3
%I EDP-Sciences
%U http://archive.numdam.org/item/ITA_1993__27_3_221_0/
%G en
%F ITA_1993__27_3_221_0
Poll, E.; Hemerik, C.; Ten Eikelder, H. M. M. CPO-models for second order lambda calculus with recursive types and subtyping. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 27 (1993) no. 3, pp. 221-260. http://archive.numdam.org/item/ITA_1993__27_3_221_0/

[ABL86] R. Amadio, K. B. Bruce and G. Longo, The finitary projection model for second order lambda calculus and higher order domain equations, Logic in Computer Science, 1986, pp. 122-135, IEEE.

[AC90] R. M. Amadio and L. Cardelli, Subtyping recursive types, Technical Report 62, Digital Systems Research Centre, 1990.

[Bar9 + ] H. P. Barendregt, Typed lambda calculi. In D. M. GABBAI, S. ABRAMSKY and T. S. E. MAIBAUM, Eds., Handbook of Logic in Computer Science, volume 1.Oxford University Press, to appear. | MR

[BH88] R. Bos and C. Hemerik, An introduction to the category-theoretic solution of recursive domain equations, Technical Report 15, Eindhoven University of Technology, 1988.

[BL90] K. B. Bruce and G. Longo, A modest model of records, iheritance and bounded quantification, Information and Computation, 1990, 87, pp. 196-240. | MR | Zbl

[BMM90] K. B. Bruce, A. R. Meyer and J. C. Mitchell, The semantics of second-order lambda calculus, Information and Computation, 1990, 85, pp. 76-134. | MR | Zbl

[BCGS91] V. Breazu-Tannen, Th. Coquand, C. A. Gunter and A. Scedrov Inheritance as explicit coercion. Information and Computation, 1991, 93, (1), pp. 172-221. | MR | Zbl

[CC91] F. Cardone and M. Coppo, Type inference with recursive types: Syntax and semantics, Information and Computation, 1991, 92, (1), pp.48-80. | MR | Zbl

[CG90] P.-L. Curien and G. Ghelli, Coherence of subsumption. In A. ARNOLD, Ed., Colloquium on Trees in Algebras and Programming, Vol. 431 of LNCS, 1990, pp. 132-146, Springer. | MR | Zbl

[CHC90] W. R. Cook, W. L. Hill and P. S. Canning, Inheritance is not subtyping, Principles of Programming Languages, 1990, pp. 125-135, ACM.

[CL90] L. Cardelli and G. Longo, A semantic basis for Quest, Technical Report 55, Digital Systems Research Center, Palo Alto, California 94301, 1990. | MR

[CM89] L. Cardelli and J. C. Mitchell, Operations on records, in M. MAIN et al., Ed., Fifth International Conference on Mathematical Foundations of Programming Semantics, Vol. 442 of LNCS, 1989, pp. 22-53.

[Cou83] B. Courcelle , Fundamental properties of infinite trees, Theoretical Computer Science, 1983, 25, pp.95-169. | MR | Zbl

[CW85] L. Cardelli and P. Wegner, On understanding types, data abstraction and polymorphism, Computing Surveys, 1985, 17, (4), pp.471-522.

[Gir72] J.-Y. Girard, Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur, Ph. D. thesis, Université Paris-VII, 1972.

[Gir86] J.-Y. Girard, The System F of variable types, fifteen years later. Theoretical Computer Science, 1986, 45, pp. 159-192. | MR | Zbl

[HS73] H. Herrlich and G. E. Strecker. Category Theory. Allyn and Bacon, 1973. | MR | Zbl

[LS81] D. J. Lehmann and M. B. Smyth, Algebraic specification of data types: a synthetic approach, Math. Syst. Theory, 1981, 11, pp. 97-139. | MR | Zbl

[McC79] N. Mccracken, An Investigation of a Programming Language with a Polymorphic Type Structure, Ph. D. thesis, Syracuse University New York, 1979.

[Mit84] J. C. Mitchell, Semantic models for second-order lambda calculus, Foundations of Computer Science, 1984, pp. 289-299, IEEE.

[MP88] J. C. Mitchell and G. D. Plotkin, Abstract types have existential type, ACM Trans. on Prog. Lang. and Syst., 1988, 10, (3), pp. 470-502.

[Pol91] E. Poll, Cpo-models for second order lambda calculus with recursive types and subtyping, Computing Science Note (91/07), Eindhoven University of Technology, 1991.

[Rey74] J. C. Reynolds, Towards a theory of type structure, Programming Symposium: Colloque sur la Programmation, LNCS, 1974, pp. 408-425, Springer. | MR | Zbl

[SP82] J. C. Smyth and G. D. Plotkin, The category-theoretic solution of recursive domain equations, S.I.A.M. Journal of Computing, 1982, 11, pp. 761-783. | MR | Zbl

[tEH89a] H. Ten Eikelder and C. Hemerik, The construction of a cpo model for second order lambda calculus with recursion, Procs, CNS'89 Computing Science in the Netherlands, 1989, pp. 131-148.

[tEH89b] H. Ten Eikelder and C. Hemerik, Some category-theoretical properties related to a model for a polymorphic lambda calculus, Computing Science Note (89/03), Eindhoven University of Technology, 1989.