article

Exact flow analysis

Author:

Christian MossinAuthors Info & Claims

Mathematical Structures in Computer Science, Volume 13, Issue 1

Pages 125 - 156

https://doi.org/10.1017/S0960129502003857

Published: 01 February 2003 Publication History

Abstract

We present a type-based flow analysis for simply typed lambda calculus with booleans, data-structures and recursion. The analysis is exact in the following sense: if the analysis predicts a redex, there exists a reduction sequence (using standard reduction plus context propagation rules) such that this redex will be reduced. The precision is accomplished using intersection typing.It follows that the analysis is non-elementary recursive – more surprisingly, the analysis is decidable. We argue that the specification of such an analysis provides a good starting point for developing new flow analyses and an important benchmark against which other flow analyses can be compared. Furthermore, we believe that the techniques employed for stating and proving exactness are of independent interest: they provide methods for reasoning about the precision of program analyses.A preliminary version of this paper has previously been published (Mossin 1997b). The present paper extends, elaborates and corrects this previously published abstract.

References

[1]

Banerjee, A. (1997) A modular, polyvariant, and type-based closure analysis. In: International Conference on Functional Programming (ICFP'97) Amsterdam, the Netherlands. SIGPLAN Notices 32 (8) 1-10.

Digital Library

[2]

Barendregt, H., Coppo, M. and Dezani-Ciancaglini, M. (1983) A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic 48 931-940.

[3]

Benton, N. (1992) Strictness analysis of lazy functional programs, Ph.D. thesis, University of Cambridge.

[4]

Coppo, M., Dezani-Ciancaglini, M. and Venneri, B. (1981) Functional characters of solvable terms. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 27 45-58.

[5]

Dussart, D., Henglein, F. and Mossin, C. (1995) Polymorphic recursion and subtype qualifications: Polymorphic binding-time analysis in polynomial time. In: Mycroft, A. (ed.) Proc. 2nd Int'l Static Analysis Symposium (SAS'95), Glasgow, Scotland. Springer-Verlag Lecture Notes in Computer Science 983 118-135.

[6]

Faxén, K.-F. (1997) Analysing, Transforming and Compiling Lazy Functional Programs, Ph. D. thesis, Royal Institute of Technology, Sweden.

[7]

Gomard, C. (1989) Higher order partial evaluation - hope for the lambda calculus. Master's thesis, DIKU, University of Copenhagen, Denmark.

[8]

Heintze, N. (1995) Control-flow analysis and type systems. In: Mycroft, A. (ed.) Proc. 2nd Int'l Static Analysis Symposium (SAS'95), Glasgow, Scotland. Springer-Verlag Lecture Notes in Computer Science 983 189-206.

[9]

Heintze, N. and McAllester, D. (1997) Linear-time Subtransitive Control Flow Analysis. In: Programming Language Design and Implementation (PLDI'97). SIGPLAN Notices 32 (5) 261- 272.

Digital Library

[10]

Henglein, F. (1994) Dynamic typing: Syntax and proof theory. Science of Computer Programming (SCP) 22 (3) 197-230.

Digital Library

[11]

Henglein, F. and Jørgensen, J. (1994) Formally optimal boxing. In: Proceedings of 21st ACM Symposium on Principles of Programming Languages (POPL'94), Oregon 213-226.

[12]

Henglein, F. and Mossin, C. (1994) Polymorphic binding-time analysis. In: Sannella, D. (ed.) Proceedings of European Symposium on Programming. Springer-Verlag Lecture Notes in Computer Science 788 287-301.

[13]

Jaganathan, S. and Weeks, S. (1995) A unified treatment of flow analysis in higher-order languages. In: Principles of Programming Languages (POPL'95), ACM Press 393-407.

[14]

Jensen, T. (1992) Abstract Interpretation in Logical Form, Ph. D. thesis, Imperial College, Univ. of London. (Available as DIKU Report 93/11.)

[15]

Jørgensen, J. (1995) A calculus for boxing analysis of polymorphically typed languages, Ph.D. thesis, DIKU, University of Copenhagen.

[16]

Kuo, T. and Mishra, P. (1987) On strictness and its analysis. In: Proc. 14th Annual ACM Symposium on Principles of Programming Languages (POPL'87) 144-155.

[17]

Kuo, T. and Mishra, P. (1989) Strictness analysis: A new perspective based on type inference. In: Proc. Functional Programming Languages and Computer Architecture (FPCA'89), London, England, ACM Press 260-272.

[18]

Leroy, X. (1992) Unboxed objects and polymorphic typing. In: Proc. 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'92), Albuquerque, New Mexico, ACM Press 177-188.

[19]

Lucassen, J.M. and Gifford, D.K. (1988) Polymorphic effect systems. In Principles of Programming Languages (POPL'88), San Diego, ACM Press 47-57.

[20]

Mossin, C. (1997a) Flow Analysis of Typed Higher-Order Programs, Ph. D. thesis, DIKU, University of Copenhagen.

[21]

Mossin, C. (1997b) Exact Flow Analysis. In: Static Analysis Symposium (SAS'97), Springer-Verlag 250-264.

[22]

Mossin, C. (1998) Higher-order value flow graphs. Nordic Journal of Computing 5 (3) 214-234.

Digital Library

[23]

Nielson, F. and Nielson, H.R. (1997) Infinitary control flow analysis: a collecting semantics for closure analysis. In: 24th Symposium on Principles of Programming Languages (POPL'97) 332-345.

[24]

Nielson, H.R. and Nielson, F. (1988) Automatic binding time analysis for a typed lambda-calculus. In: Fifteenth ACM Symposium on Principles of Programming Languages (POPL'88), ACM Press 98-106. (Extended Abstract.)

[25]

Palsberg, J. (1994) Global program analysis in constraint form. In: Tison, S. (ed.) 19th International Colloquium on Trees in Algebra and Programming (CAAP'94). Springer-Verlag Lecture Notes in Computer Science 787 276-290.

[26]

Palsberg, J. and O'Keefe, P. (1995) A type system equivalent to flow analysis. In: Principles of Programming Languages (POPL'95), San Francisco 367-378.

[27]

Sestoft, P. (1991) Analysis and Efficient Implementation of Functional Languages, Ph. D. thesis, DIKU, University of Copenhagen.

[28]

Shivers, O. (1991) Control-Flow Analysis of Higher-Order Languages, Ph. D. thesis, Carnegie Mellon University. (CMU-CS-91-145.)

[29]

Solberg, K.L. (1994) Strictness and totality analysis In: Symposium on Static Analysis (SAS'94). Springer-Verlag Lecture Notes in Computer Science 864 408-422.

[30]

Solberg, K.L. (1995) Strictness and totality analysis. In: Theory and Practice of Software Development (TAPSOFT'95). Springer-Verlag Lecture Notes in Computer Science 915 501-515.

[31]

Statman, R. (1979) The typed ¿-calculus is not elementary recursive. Theoretical Computer Science 9 (1) 73-81.

[32]

Talpin, J.-P. and Jouvelot, P. (1994) The type and effect discipline. Information and Computation 111 245-296.

Digital Library

[33]

van Bakel, S. (1995) Intersection type assignment systems. Theoretical Computer Science 151 (2) 385-435.

Digital Library

[34]

Wright, D. (1991) A new technique for strictness analysis. In: Theory and Practice of Software Development (TAPSOFT'91). Springer-Verlag Lecture Notes in Computer Science 494 235-258.

Cited By

Shen XZheng KEmrouznejad AXu Z(2019)Characterizing Strongly Normalizing λGtz-terms via Non-Idempotent Intersection TypesProceedings of the 3rd International Conference on Computer Science and Application Engineering10.1145/3331453.3360959(1-7)Online publication date: 22-Oct-2019
https://dl.acm.org/doi/10.1145/3331453.3360959
Kobayashi N(2013)Model Checking Higher-Order ProgramsJournal of the ACM10.1145/2487241.248724660:3(1-62)Online publication date: 1-Jun-2013
https://dl.acm.org/doi/10.1145/2487241.2487246
Midtgaard J(2012)Control-flow analysis of functional programsACM Computing Surveys10.1145/2187671.218767244:3(1-33)Online publication date: 14-Jun-2012
https://dl.acm.org/doi/10.1145/2187671.2187672
Show More Cited By

Index Terms

Exact flow analysis
1. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program semantics

Index terms have been assigned to the content through auto-classification.

Recommendations

Exact flow analysis by higher-order model checking
FLOPS'12: Proceedings of the 11th international conference on Functional and Logic Programming

We propose a novel control flow analysis for higher-order functional programs, based on a reduction to higher-order model checking. The distinguished features of our control flow analysis are that, unlike most of the control flow analyses like <em>k</em>...
Logic-flow analysis of higher-order programs
POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

This work presents a framework for fusing flow analysis and theorem proving called logic-flow analysis (LFA). The framework itself is the reduced product of two abstract interpretations: (1) an abstract state machine and (2) a set of propositions in a ...
Logic-flow analysis of higher-order programs
Proceedings of the 2007 POPL Conference

This work presents a framework for fusing flow analysis and theorem proving called logic-flow analysis (LFA). The framework itself is the reduced product of two abstract interpretations: (1) an abstract state machine and (2) a set of propositions in a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Mathematical Structures in Computer Science

Mathematical Structures in Computer Science Volume 13, Issue 1

February 2003

193 pages

ISSN:0960-1295

Issue’s Table of Contents

Publisher

Cambridge University Press

United States

Publication History

Published: 01 February 2003

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 24 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Shen XZheng KEmrouznejad AXu Z(2019)Characterizing Strongly Normalizing λGtz-terms via Non-Idempotent Intersection TypesProceedings of the 3rd International Conference on Computer Science and Application Engineering10.1145/3331453.3360959(1-7)Online publication date: 22-Oct-2019
https://dl.acm.org/doi/10.1145/3331453.3360959
Kobayashi N(2013)Model Checking Higher-Order ProgramsJournal of the ACM10.1145/2487241.248724660:3(1-62)Online publication date: 1-Jun-2013
https://dl.acm.org/doi/10.1145/2487241.2487246
Midtgaard J(2012)Control-flow analysis of functional programsACM Computing Surveys10.1145/2187671.218767244:3(1-33)Online publication date: 14-Jun-2012
https://dl.acm.org/doi/10.1145/2187671.2187672
Tobita YTsukada TKobayashi N(2012)Exact flow analysis by higher-order model checkingProceedings of the 11th international conference on Functional and Logic Programming10.1007/978-3-642-29822-6_22(275-289)Online publication date: 23-May-2012
https://dl.acm.org/doi/10.1007/978-3-642-29822-6_22
Holdermans SHage J(2010)Polyvariant flow analysis with higher-ranked polymorphic types and higher-order effect operatorsACM SIGPLAN Notices10.1145/1932681.186355445:9(63-74)Online publication date: 27-Sep-2010
https://dl.acm.org/doi/10.1145/1932681.1863554
Holdermans SHage JHudak PWeirich S(2010)Polyvariant flow analysis with higher-ranked polymorphic types and higher-order effect operatorsProceedings of the 15th ACM SIGPLAN international conference on Functional programming10.1145/1863543.1863554(63-74)Online publication date: 27-Sep-2010
https://dl.acm.org/doi/10.1145/1863543.1863554
Neergaard PMairson HOkasaki CFisher K(2004)Types, potency, and idempotencyProceedings of the ninth ACM SIGPLAN international conference on Functional programming10.1145/1016850.1016871(138-149)Online publication date: 19-Sep-2004
https://dl.acm.org/doi/10.1145/1016850.1016871
Neergaard PMairson H(2004)Types, potency, and idempotencyACM SIGPLAN Notices10.1145/1016848.101687139:9(138-149)Online publication date: 19-Sep-2004
https://dl.acm.org/doi/10.1145/1016848.1016871

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents