Abstract
We introduce a variant of the system of rank 2 intersection types with new typing rules for local definitions (let-expressions and letrec-expressions) and conditional expressions (if-expressions and case-expressions). These extensions are a further step towards the use of intersection types in “real” programming languages.
Chapter PDF
References
S. Aditya and R. Nikhil. Incremental polymorphism. In POPL’93, LNCS 523, pages 379–405. Springer-Verlag, 1991.
M. Coppo and P. Giannini. Principal Types and Unification for Simple Intersection Types Systems. Information and Computation, 122(1):70–96, 1995.
L. M. M. Damas and R. Milner. Principal type schemas for functional programs. In POPL’82, pages 207–212. ACM, 1982.
F. Damiani and P. Giannini. A Decidable Intersection Type System based on Relevance. In TACS’94, LNCS 789, pages 707–725. Springer-Verlag, 1994.
R. Hindley. Basic Simple Type Theory. Number 42 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, London, 1997.
T. Jim. Rank 2 type systems and recursive definitions. Technical Report MIT/LCS/TM-531, LCS, Massachusetts Institute of Technology, 1995.
T. Jim. What are principal typings and what are they good for? In POPL’96, pages 42–53. ACM, 1996.
A. J. Kfoury and J. B. Wells. A direct algorithm for type inference in the rank-2 fragment of the second-order lambda-calculus. In LISP and Functional Programming’ 94. ACM, 1994.
A. J. Kfoury and J. B. Wells. Principality and Decidable Type Inference for Finite-Rank Intersection Types. In POPL’99. ACM, 1999.
D. Leivant. Polymorphic Type Inference. In POPL’83. ACM, 1983.
R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML-Revised. MIT press, 1997.
A. Mycroft. Polymorphic Type Schemes and Recursive Definitions. In International Symposium on Programming, LNCS 167, pages 217–228. Springer-Verlag, 1984.
Z. Shao and A. W. Appel. Smartest recompilation. In POPL’93, pages 439–450. ACM, 1993.
S. van Bakel. Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems. PhD thesis, Katholieke Universiteit Nijmegen, 1993.
H. Yokouchi. Embedding a Second-Order Type System into an Intersection Type System. Information and Computation, 117:206–220, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Damiani, F. (2000). Typing Local Definitions and Conditional Expressions with Rank 2 Intersection (Extended Abstract). In: Tiuryn, J. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2000. Lecture Notes in Computer Science, vol 1784. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46432-8_6
Download citation
DOI: https://doi.org/10.1007/3-540-46432-8_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67257-9
Online ISBN: 978-3-540-46432-7
eBook Packages: Springer Book Archive