Hostname: page-component-586b7cd67f-2plfb Total loading time: 0 Render date: 2024-11-22T06:46:26.008Z Has data issue: false hasContentIssue false
  • English
  • Français

Strong normalization with non-structural subtyping

Published online by Cambridge University Press:  04 March 2009

Mitchell Wand ,
Patrick O'Keefe  and
Jens Palsberg
Mitchell Wand
Affiliation:
College of Computer Science, Northeastern University, 360 Huntington Avenue, 161CN, Boston, MA 02115, USA. E-mail: [email protected]
Patrick O'Keefe
Affiliation:
151 Coolidge Avenue #211, Watertown, MA 02172, USA. E-mail: [email protected]
Jens Palsberg
Affiliation:
Computer Science Department, Aarhus University, DK-8000 Aarhus C, Denmark. E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We study a type system with a notion of subtyping that involves a largest type ⊤, a smallest type ⊥, atomic coercions between base types, and the usual ordering of function types. We prove that any λ-term typable in this system is strongly normalizing, which solves an open problem of Thatte. We also prove that the fragment without ⊥ types has strictly fewer terms. This demonstrates that ⊥ adds power to a type system.

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 5 , Issue 3 , September 1995 , pp. 419 - 429
Copyright
Copyright © Cambridge University Press 1995

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Amadio, R. M. and Cardelli, L. (1993) Subtyping recursive types. ACM Transactions on Programming Languages and Systems 15 (4) 575–631. (Also in Proc. POPL’91.)CrossRefGoogle Scholar
Giannini, P. and Ronchi Della Rocca, S. (1988) Characterization of typings in polymorphic type discipline. Proc. LICS’88, Third Annual Symposium on Logic in Computer Science 61–70.CrossRefGoogle Scholar
Gomard, C. K. (1990) Partial type inference for untyped functional programs. Proc. ACM Conference on Lisp and Functional Programming 282–287.CrossRefGoogle Scholar
Kozen, D., Palsberg, J. and Schwartzbach, M. I. (1994) Efficient inference of partial types. Journal of Computer and System Sciences 49 (2) 306–324.(Also in Proc. FOCS’92, 33rd IEEE Symposium on Foundations of Computer Science, October 1992, Pittsburgh, Pennsylvania, 363–371.)CrossRefGoogle Scholar
Mitchell, J. C. (1991) Type inference with simple subtypes. Journal of Functional Programming 1 245–285.CrossRefGoogle Scholar
O’Keefe, P. M. and Wand, M. (1992) Type inference for partial types is decidable. Proc. ESOP’92, European Symposium on Programming. Springer-Verlag Lecture Notes in Computer Science 582 408–417.CrossRefGoogle Scholar
Palsberg, J. and Schwartzbach, M. I. (1992) Safety analysis versus type inference for partial types. Information Processing Letters 43 175–180.CrossRefGoogle Scholar
Rémy, D. (1989) Typechecking records and variants in a natural extension of ML. Sixteenth Symposium on Principles of Programming Languages 77–88.Google Scholar
Thatte, S. (1988) Type inference with partial types. Proc. International Colloquium on Automata, Languages, and Programming 1988. Springer-Verlag Lecture Notes in Computer Science 317 615–629.CrossRefGoogle Scholar
Wand, M. (1984) A semantic prototyping system. Proc. ACM SIGPLAN’84 Symposium on Compiler Construction, Sigplan Notices 213–221.CrossRefGoogle Scholar
Wand, M. (1991) Type inference for record concatenation and multiple inheritance. Information and Computation 93 (1) 1–15.CrossRefGoogle Scholar