CPO-models for second order lambda calculus with recursive types and subtyping
Poll, E. ; Hemerik, C. ; Ten Eikelder, H. M. M.
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 27 (1993), p. 221-260 / Harvested from Numdam
Access to full text
Full (PDF)
Full (DJVU)
Publié le : 1993-01-01
@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},
     volume = {27},
     year = {1993},
     pages = {221-260},
     mrnumber = {1227944},
     zbl = {0788.03016},
     language = {en},
     url = {http://dml.mathdoc.fr/item/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) pp. 221-260. http://gdmltest.u-ga.fr/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 1381697

[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 1055952 | Zbl 0711.68072

[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 1042650 | Zbl 0714.68052

[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 1115265 | Zbl 0799.68129

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

[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 1075027 | Zbl 0759.03009

[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 1140339

[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 693076 | Zbl 0521.68013

[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 867281 | Zbl 0623.03013

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

[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 616960 | Zbl 0457.68035

[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 458988 | Zbl 0309.68016

[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 677666 | Zbl 0493.68022

[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.