Abstract
Strictness analysis has been an active field of research since strictness information is of great importance for generating efficient code for lazy functional languages.
One of the most efficient and precise methods for strictness analysis is abstract reduction. Abstract reduction is able to find strictness information in a language with higher-order functions and structured data types. We present a tableau-based calculus for abstract reduction on a lazy functional core language. This approach permits us to prove soundness in an easy and transparent way, and also provides a soundness proof for existing implementations of abstract reduction.
We would like to thank Florian Panitz for correcting some of the spelling errors and his advice on language use.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, pages 252–252. ACM Press, 1977.
Denis B Howe and Geoffrey L Burn. Using strictness in the STG machine. In John T O'Donnel and Kevin Hammond, editors, Functional Programming, Workshops in Computingt, pages 127–137. Springer, 1993.
P. H. Hartel, M. Feeley, M. Alt, L. Augustsson, P. Baumann, M. Beemster, E. Chailloux, C. H. Flood, W. Grieskamp, J. H. G. van Groningen, K. Hammond, B. Hausman, M.Y. Ivory, P. Lee, X. Leroy, S: Loosemore, N. Röjemo, M. Serrano, J.-P. Talpin, J. Thackray, P. Weiss, and P. Wentworth. Pseudoknot: a float-intensive benchmark for functional compilers. In John Glauert, editor, Implementation of Functional Languages '94, 1994. Draft.
Kristian Damm Jensen, Peter Hjæresen, and Mads Rosendahl. Efficient strictness analysis of Haskell. In Baudouin Le Charlier, editor, Static Analysis, number 864 in Lecture Notes in Computer Science, pages 346–362. Springer, 1994.
Mark P. Jones. The implementation of the Gofer functional programming system. Research Report YALEU/DCS/RR-1030, Yale University, Department of Computer Science, May 1994.
Alan Mycroft. The theory and practice of transforming call-by-need into call-by-value. In 4th International Symposium on Programming, number 83 in Lecture Notes in Computer Science, pages 269–281. Springer, 1980.
Eric Nöcker. Strictness analysis by abstract reduction in orthogonal term rewriting systems. Technical Report 92-31, University of Nijmegen, Department of Computer Science, 1992.
Eric Nöcker. Strictness analysis using abstract reduction. In Functional Programming Languages and Computer Architecture, pages 255–265. ACM Press, 1993.
E. G. J. M. H. Nöcker, J. E. W. Smetsers, M. C. J. D. van Eekelen, and M. J. Plasmeijer. Concurrent Clean. In Springer Verlag, editor, Proc of Parallel Architecture and Languages Europe (PARLE'91), number 505 in Lecture Notes in Computer Science, pages 202–219, 1991.
Simon L. Peyton Jones and John Launchbury. Unboxed values as first class citizens in a non-strict functional language. In Functional Programming Languages and Computer Architecture, number 523 in Lecture Notes in Computer Science, pages 636–666. Springer, 1991.
Simon L. Peyton Jones and David R. Lester. Implementing Functional Languages: a Tutorial. Prentice-Hall International, London, 1991.
Simon L. Peyton Jones and André Santos. Compilation by transformation in the Glasgow Haskell Compiler. In Functional Programming, Glasgow 1994, Workshops in Computing, pages 184–204. Springer, 1994.
Rinus Plasmeijer and Marko van Eekelen. Functional Programming and Parallel Graph Rewriting. Addison-Wesley, Workingham, 1993.
Marko Schütz. Striktheits-Analyse mittels abstrakter Reduktion für den Sprachkern einer nicht-strikten funktionalen Programmiersprache. Master's thesis, Johann Wolfgang Goethe-Universität, Frankfurt, 1994. in German.
Marko Schütz. The G#-machine: Efficient strictness analysis in Haskell. Technical Report 1/95, Johann Wolfgang Goethe-Universität, Fachbereich Informatik, January 1995.
Raymond M. Smullyan. First-Order Logic. Springer, 1971.
M. van Eekelen, E. Goubault, C.L. Hankin, and E. Nöcker. Abstract reduction: Towards a theory via abstract interpretation. In M.R. Sleep, M.J. Plasmeijer, and M.C.J.D. van Eekelen, editors, Term Graph Rewriting-Theory and Practice, chapter 9. Wiley, Chichester, 1993.
Phil Wadler. Strictness analysis on non-flat domains (by abstract interpretation over finite domains). In Samson Abramsky and Chris Hankin, editors, Abstract Interpretation of Declerative Languages, chapter 12. Ellis Horwood Limited, Chichester, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schmidt-Schauß, M., Panitz, S.E., Schütz, M. (1995). Strictness analysis by abstract reduction using a tableau calculus. In: Mycroft, A. (eds) Static Analysis. SAS 1995. Lecture Notes in Computer Science, vol 983. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60360-3_49
Download citation
DOI: https://doi.org/10.1007/3-540-60360-3_49
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60360-3
Online ISBN: 978-3-540-45050-4
eBook Packages: Springer Book Archive