Abstract
We present a type-based specification for useless-variable elimination for a higher-order, call-by-value functional language. Utilizing a weak form of dependent types, we introduce a mechanism for eliminating at runtime useless code that is not detectable statically. We prove the specifications sound and safe with respect to an operational semantics, ensuring that eliminated expressions contributed no observable behavior to the original program. We define an algorithm that implements useless-variable elimination without dependent types, and we prove this algorithm correct with respect to the specification.
Article
This work is supported in part by NSF Award #CCR-9900918.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Beradi, S., Coppo, M., Damiani, F., and Giannini, P. Type-based useless-code elimination for functional programs. In Semantics, Applications, and Implementation of Program Generation (September 2000), W. Taha, Ed., no. 1924 in Lecture Notes in Computer Science, Springer-Verlag.
Damiani, F. Conjunctive types and useless-code elimination. In ICALP Workshops (2000), vol. 8 of Proceedings in Informatics, Carleton-Scientific, pp. 271–285.
Damiani, F., and Giannini, P. Automatic useless-code elimination for HOT functional languages. Journal of Functional Programming (2000). (to appear).
Fischbach, A., and Hannan, J. Type systems for useless-variable elimination. Tech. Rept. CSE-01-002. Penn State University.
Hannan, J., and Hicks, P. Higher-order arity raising. In Proceedings of the Third International Conference on Functional Programming (September 1998), P. Hudak and C. Queinnec, Eds., ACM SIGPLAN, pp. 27–38.
Hannan, J., and Hicks, P. Higher-order unCurrying. In Proceedings of the 25th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (January 1998), pp. 1–11.
Kobayashi, N. Type-based useless-variable elimination. In Proceedings of the 2000 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (2000), pp. 84–93.
Shivers, O. Control-Flow Analysis of Higher-Order Languages. PhD thesis, Carnegie-Mellon University, May 1991.
Wand, M., and Siveroni, I. Constraint systems for useless variable elimination. In Conf. Rec. 26th ACM Symposium on Principles of Programming Languages (1999).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fischbach, A., Hannan, J. (2001). Type Systems for Useless-Variable Elimination. In: Danvy, O., Filinski, A. (eds) Programs as Data Objects. PADO 2001. Lecture Notes in Computer Science, vol 2053. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44978-7_3
Download citation
DOI: https://doi.org/10.1007/3-540-44978-7_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42068-2
Online ISBN: 978-3-540-44978-2
eBook Packages: Springer Book Archive