Abstract
We describe a logic for reasoning about higher-order strictness properties of typed lambda terms. The logic arises from axiomatising the inclusion order on certain closed subsets of domains. The axiomatisation of the lattice of strictness properties is shown to be sound and complete, and we then give a program logic for assigning properties to terms. This places work on strictness analysis via type inference on a firm theoretical foundation. We then use proof theoretic techniques to show how the derivable strictness properties of different instances of polymorphically typed terms are related.
Research supported by a SERC Research Studentship.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Samson Abramsky. Strictness analysis and polymorphic invariance (extended abstract). In H. Ganzinger and N. Jones, editors, Proceedings of the Workshop on Programs as Data Objects, Copenhagen, volume 217 of Lecture Notes in Computer Science, pages 1–23. Springer-Verlag, October 1985.
Samson Abramsky. Domain theory in logical form. Annals of Pure and Applied Logic, 51(1–2):1–78, 1991.
Samson Abramsky and Thomas P. Jensen. A relational approach to strictness analysis of higher order polymorphic functions. In Proceedings of ACM Symposium on Principles of Programming Languages, 1991.
P. N. Benton. Static Analyses and Optimising Transformations for Lazy Functional Programs. PhD thesis, University of Cambridge, 1992. in preparation.
Geoffrey L. Burn, Chris L. Hankin, and Samson Abramsky. The theory of strictness analysis for higher order functions. In H. Ganzinger and N. Jones, editors, Proceedings of the Workshop on Programs as Data Objects, Copenhagen, volume 217 of Lecture Notes in Computer Science. Springer-Verlag, October 1985.
R.J.M. Hughes. Abstract interpretation of first-order polymorphic functions. In Glasgow Workshop on Functional Programming, August 1988.
Thomas P. Jensen. Strictness analysis in logical form. In Proceedings of the 1991 Conference on Functional Programming Languages and Computer Architecture, 1991.
P. T. Johnstone. Stone Spaces. Cambridge studies in advanced mathematics. Cambridge University Press, 1982.
T.-M. Kuo and P. Mishra. Strictness analysis: A new perspective based on type inference. In Proceedings of the 4th International Conference on Functional Programming Languages and Computer Architecture. ACM, 1989.
John C. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 8, pages 365–458. Elsevier Science Publishers, 1990.
Alan Mycroft. Abstract Interpretation and Optimising Transformations for Applicative Programs. PhD thesis, Department of Computer Science, University of Edinburgh, December 1981.
Alan Mycroft and Neil D. Jones. A relational framework for abstract interpretation. In H. Ganzinger and N. Jones, editors, Proceedings of the Workshop on Programs as Data Objects, Copenhagen, volume 217 of Lecture Notes in Computer Science. Springer-Verlag, October 1985.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Benton, P.N. (1992). Strictness logic and polymorphic invariance. In: Nerode, A., Taitslin, M. (eds) Logical Foundations of Computer Science — Tver '92. LFCS 1992. Lecture Notes in Computer Science, vol 620. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023861
Download citation
DOI: https://doi.org/10.1007/BFb0023861
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55707-4
Online ISBN: 978-3-540-47276-6
eBook Packages: Springer Book Archive