Abstract
We develop a system of type assignment with intersection types, union types, indexed types, and universal and existential dependent types that is sound in a call-by-value functional language. The combination of logical and computational principles underlying our formulation naturally leads to the central idea of type-checking subterms in evaluation order. We thereby provide a uniform generalization and explanation of several earlier isolated systems. The proof of progress and type preservation, usually formulated for closed terms only, relies on a notion of definite substitution.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alexander Aiken, Edward L. Wimmers, and T. K. Lakshman. Soft typing with conditional types. In Proc. 21st Symposium on Principles of Programming Languages (POPL’ 94), pages 163–173, 1994.
Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Ugo de'Liguoro. Intersection and union types: syntax and semantics. Inf. and Comp., 119:202–230, 1995.
R. Cartwright and M. Fagan. Soft typing. In Proc. SIGPLAN’ 91 Conf. Programming Language Design and Impl. (PLDI), volume 26, pages 278–292, 1991.
M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Functional characters of solvable terms. Zeitschrift f. math. Logik und Grundlagen d. Math., 27:45–58, 1981.
Rowan Davies. Practical refinement-type checking. PhD thesis proposal, Carnegie Mellon University, 1997.
Rowan Davies and Frank Pfenning. Intersection types and computational effects. In Proc. Int’l Conf. Functional Programming (ICFP’ 00), pages 198–208, 2000.
Jana Dunfield. Combining two forms of type refinements. Technical Report CMU-CS-02-182, Carnegie Mellon University, September 2002.
Tim Freeman and Frank Pfenning. Refinement types for ML. In Proc. SIGPLAN’ 91 Conf. Programming Language Design and Impl. (PLDI), volume 26, pages 268–277. ACM Press, June 1991.
Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.
Jens Palsberg and Christina Pavlopoulou. From polyvariant flow information to intersection and union types. J. Functional Programming, 11(3):263–317, 2001.
Benjamin C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, 1991.
John C. Reynolds. Design of the programming language Forsythe. Technical Report CMU-CS-96-146, Carnegie Mellon University, 1996.
S. van Bakel, M. Dezani-Ciancaglini, U. de'Liguoro, and Y. Motohoma. The minimal relevant logic and the call-by-value lambda calculus. To appear, July 1999.
J.B. Wells, Allyn Dimock, Robert Muller, and Franklyn Turbak. A calculus with polymorphic and polyvariant flow types. J. Functional Programming, 12(3):183–317, May 2002.
Hongwei Xi. Dependent types in practical programming. PhD thesis, Carnegie Mellon University, 1998.
Hongwei Xi. Dependently typed data structures. Revised version superseding that of WAAAPL’ 99, available electronically, February 2000.
Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In Proc. 26th Symp. on Principles of Programming Languages (POPL’99), pages 214–227. ACM Press, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dunfield, J., Pfenning, F. (2003). Type Assignment for Intersections and Unions in Call-by-Value Languages. In: Gordon, A.D. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2003. Lecture Notes in Computer Science, vol 2620. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36576-1_16
Download citation
DOI: https://doi.org/10.1007/3-540-36576-1_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00897-2
Online ISBN: 978-3-540-36576-1
eBook Packages: Springer Book Archive