Abstract
We present a typed intermediate language λCIL for optimizing compilers for function-oriented and polymorphically typed programming languages (e.g., ML). The language λCIL is a typed lambda calculus with product, sum, intersection, and union types as well as function types annotated with flow labels. A novel formulation of intersection and union types supports encoding flow information in the typed program representation. This flow information can direct optimization.
Supported by NSF grant CCR-9417382.
Chapter PDF
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
A. S. Aiken and E. L. Wimmers. Type inclusion constraints and type inference. In FPCA '93, Conf. Funct. Program. Lang. Comput. Arch., pp. 31–41. ACM, 1993.
A. S. Aiken, E. L. Wimmers, and T. K. Lakshman. Soft typing with conditional types. In POPL '94 [22], pp. 163–173.
A. W. Appel. Compiling with Continuations. Cambridge University Press, 1992.
S. van Bakel. Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems. PhD thesis, University of Nijmegen, 1993.
A. Banerjee. A modular, polyvariant, and type-based closure analysis. Manuscript, Nov. 1996.
F. Barbanera and M. Dezani-Ciancaglini. Intersection and union types: Syntax and semantics. Information and Computation, 119:202–230, 1995.
N. S. BjØrner. Minimal typing derivations. In ACM SIGPLAN Workshop on ML and its Applications, pp. 120–126, 1994.
A. Dimock, R. Muller, F. Turbak, and J. B. Wells. Strongly typed flow-directed representation transformations (extended abstract). Submitted. See http://www.cs.bu.edu/groups/church, Nov. 1996.
J.-Y. Girard. Interprétation Fonctionnelle et Elimination des Coupures de l'Arithmétique d'Ordre Supérieur. Thèse d'Etat, Université de Paris VII, 1972.
J. Hannan. Type systems for closure conversion. In Workshop on Types for Program Analysis, pp. 48–62, 1995. DAIMI PB-493.
R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. In Conf. Rec. 22nd Ann. ACM Symp. Principles of Programming Languages, 1995.
N. Heintze. Control-flow analysis and type systems. In Proc. 2nd Int'l Static Analysis Symp., pp. 189–206, 1995.
T. Jim. What are principal typings and what are they good for? In POPL '96 [23].
M. P. Jones. Dictionary-free overloading by partial evaluation. In ACM SIGPLAN Workshop on Partial Eval. & Semantics-Based Prog. Manipulation, 1994.
S. L. P. Jones. Compiling Haskell by program transformation: a report from the trenches. In Proc. European Symp. on Programming, 1996.
X. Leroy. Unboxed objects and polymorphic typing. In Conf. Rec. 19th Ann. ACM Symp. Principles of Programming Languages, pp. 177–188, 1992.
Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. In POPL '96 [23].
G. Morrisett. Compiling with Types. PhD thesis, Carnegie Mellon University, 1995.
S. Peyton Jones and E. Meijer. Henk: A typed intermediate language. Submitted, Jan. 1997.
B. C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, Feb. 1991.
Proc. ACM SIGPLAN '95 Conf. Prog. Language Design & Implementation, 1995.
Conf. Rec. 21st Ann. ACM Symp. Principles of Programming Languages, 1994.
Conf. Rec. POPL '96: 23rd ACM Symp. Principles of Prog. Languages, 1996.
J. C. Reynolds. Towards a theory of type structure. In Colloque sur la Programmation, vol. 19 of LNCS, pp. 408–425, Paris, France, 1974. Springer-Verlag.
J. C. Reynolds. Design of the programming language Forsythe. In P. O'Hearn and R. D. Tennent, eds., Algol-like Languages. Birkhauser, 1996.
Z. Shao. Compiling Standard ML for Efficient Execution on Modern Machines. PhD thesis, Princeton University, 1994.
Z. Shao and A. Appel. A type-based compiler for Standard ML. In PLDI '95 [21].
D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: A type-directed optimizing compiler for ML. In PLDI '95 [21].
V. Trifonov and S. Smith. Subtyping constrained types. Revised Draft, May 1996.
M. Wand and P. Steckler. Selective and lightweight closure conversion In POPL '94 [22], pp. 435–445.
J. B. Wells. Intersection types revisited in the Church style. Manuscript, June 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wells, J.B., Dimock, A., Muller, R., Turbak, F. (1997). A typed intermediate language for flow-directed compilation. In: Bidoit, M., Dauchet, M. (eds) TAPSOFT '97: Theory and Practice of Software Development. CAAP 1997. Lecture Notes in Computer Science, vol 1214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0030639
Download citation
DOI: https://doi.org/10.1007/BFb0030639
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62781-4
Online ISBN: 978-3-540-68517-3
eBook Packages: Springer Book Archive