- 1.A. Arnold and M. Nivat, "Metric interpretations of finite trees and semantics of nondeterministic recursive programs," Theoretical Computer Science11, pp. 181-205 (1980).Google Scholar
- 2.S. Banach, "Sur les opérations dans les ensembles abstraits et leurs applications aux équations intégrales," Fund. Math.3, pp. 7-33 (1922).Google ScholarCross Ref
- 3.R. M. Burstall, D. B. MacQueen, and D. T. Sanella, "Hope: an experimental applicative language," Lisp Conference, Stanford, pp. 136-143 (August 1980). Google ScholarDigital Library
- 4.L. Damas and R. Milner, "Principal type-schemes for functional programs," Ninth Annual ACM Symposium on Principles of Programming Languages, Albuquerque NM, pp. 207-212 (January 1982). Google ScholarDigital Library
- 5.J. W. deBakker and J. I. Zucker, "Processes and the denotational semantics of concurrency," Information and Control54, pp. 70-120 (1982).Google Scholar
- 6.M. J. Gordon, A. J. Milner, and C. P. Wadsworth, Edinburgh LCF, Lecture Notes in Computer Science 78 (1979).Google Scholar
- 7.P. Henderson, "An approach to compile-time type checking," pp. 523-527 in Information Processing 77, ed. B. Gilchrist, North-Holland (1977).Google Scholar
- 8.R. Hindley, "The principal type-scheme of an object in combinatory logic," Trans. AMS146, pp. 29-60 (December 1969).Google Scholar
- 9.J. E. Hopcroft and R. M. Karp, "An algorithm for testing the equivalence of finite automata," TR-71-114, Dept. of Computer Science, Cornell Univ. (1971).Google Scholar
- 10.D. E. Knuth, The Art of Computer Programming: Volume 1, Fundamental Algorithms, Addison-Wesley, Reading MA (1968). Google ScholarDigital Library
- 11.D. B. MacQueen and R. Sethi, "A higher order polymorphic type system for applicative languages," 1982 Symposium on Lisp and Functional Programming, Pittsburgh PA, pp. 243-252 (August 1982). Google ScholarDigital Library
- 12.N. J. McCracken, "An investigation of a programming language with a polymorphic type structure," Ph.D. Thesis, Computer and Information Science, Syracuse Univ. (June 1979). Google ScholarDigital Library
- 13.R. Milner, "A theory of type polymorphism in programming," >JCSS17(3), pp. 348-375 (December 1978).Google Scholar
- 14.F. L. Morris, "Automatic assignment of concrete type schemes to programs," unpublished (197?).Google Scholar
- 15.F.L. Morris, "On list structures and their use in the programming of unification," Report 4-78, School of Computer and Information Science, Syracuse Univ. (August 1978). A fast algorithm for circular unification is credited to G. Huet, G. Kahn, and J. A. Robinson.Google Scholar
- 16.J. H. Morris Jr., "Lambda-calculus models of programming languages," Ph.D. Thesis, Sloan School of Management, MIT (1968).Google Scholar
- 17.G. Plotkin, "Advanced domains," Summer School, Pisa (1978).Google Scholar
- 18.J. C. Reynolds, "Towards a theory of type structure," pp. 408-425 in Programming Symposium, Paris, 1974, Lecture Notes in Computer Science 19, Springer Verlag, Berlin (1974). Google ScholarDigital Library
- 19.J. A. Robinson, "A machine-oriented logic based on the resolution principle," J. ACM12, pp. 23-41 (1965). Google ScholarDigital Library
- 20.D. S. Scott, "Continuous lattices," pp. 97-136 in Lecture Notes in Mathematics274 (1972).Google Scholar
- 21.A. Shamir and W. W. Wadge, "Data types as objects," pp. 465-479 in Automata, Languages and Programming, 4th Colloquium, Turku, Lecture Notes in Computer Science 52, Springer-Verlag, Berlin (1977). Google ScholarDigital Library
- 22.W. W. Wadge, Personal communication to R. Milner, March 1978.Google Scholar
- 23.M. Wand, personal communication, January 1983.Google Scholar
Index Terms
- An ideal model for recursive polymorphic types
Recommendations
Subtyping recursive types
We investigate the interactions of subtyping and recursive types, in a simply typed λ-calculus. The two fundamental questions here are whether two (recursive)types are in the subtype relation and whether a term has a type. To address the first question, ...
Set-theoretic types for polymorphic variants
ICFP '16Polymorphic variants are a useful feature of the OCaml language whose current definition and implementation rely on kinding constraints to simulate a subtyping relation via unification. This yields an awkward formalization and results in a type system ...
Comments