More Web Proxy on the site http://driver.im/

article

Open access

Collecting interpretations of expressions

Authors:

Jonathan YoungAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 13, Issue 2

Pages 269 - 290

https://doi.org/10.1145/103135.103139

Published: 01 April 1991 Publication History

Abstract

A collecting interpretation of expressions is an interpretation of a program that allows one to answer questions of the sort: “What are all possible values to which an expression might evaluate during program execution?” Answering such questions in a denotational framework is akin to traditional data flow analysis and, when used in the context of abstract interpretation, allows one to infer properties that approximate the run-time behavior of expression evaluation.

Exact collecting interpretations of expressions are developed for three abstract functional languages: a strict first-order language, a nonstrict first-order language, and a nonstrict higher order language (the full untyped lambda calculus with constants). It is argued that the method is simple (in particular, no powerdomains are needed), Natural (it captures the intuitive operational behavior of a cache), yet more expressive than existing methods (it is the first exact collecting interpretation for either nonstrict higher order languages). Correctness of the interpretations with respect to the standard semantics is shown via a generalization of the notion of strictness. It is further shown how to form abstractions of these exact interpretations, using as an example a collecting strictness analysis which yields compile-time information not previously captured by conventional strictness analyses.

References

[1]

ASRAMSKY, S. AND HANKIN C. Abstract Interpretation of Declarative Languages. Ellis Horwood, Chichester, England, 1987.

Digital Library

[2]

BURN, G. L, HANKIN, C. L. AND ABRAMSKY, S. The theory of strictness analysis for higher order functions. In Lecture Notes in Computer Science, vol. 217: Programs as Data Objects. Springer-Verlag, New York, 1985, pp. 42-62.

Digital Library

[3]

COUSOT, P. AND COUSOT, R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings ofthe 4th ACM Symposium on Principles of Programming Languages. ACM, New York, 1977, pp. 238-252.

Digital Library

[4]

COUSOT, P., ANV COUSOT, R. Systematic design of program analysis frameworks. In Proceedings of the 6th ACM Symposium on Principles of Programming Languages. ACM, New York, pp. 269-282.

Digital Library

[5]

DONZEAU-GOuGE, V. Denotational definition of properties of program computations. In Program Flow Analysis: Theory and Applications. Prentice-Hall, Englewood Cliffs, N.J., pp. 343-379.

[6]

FAIRBAIRN, J. AND WRAY, S. C. Code generation techniques for functional languages. In Proceedmgs 1986 ACM Conference on Lisp and Functional Programming, (Cambridge, Mass., Aug. 1986). ACM, New York, 1986, pp. 94-104.

Digital Library

[7]

GOLDBERG, B., AND HUnAK, P. Detecting sharing of partial applications in functional languages. YALEU/DCS/RR-526, Dept. Computer Science, Yale University, New Haven, Conn., Mar. 1987.

[8]

HUDAK, P. A semantic model of reference counting and its abstraction (detailed summary). In Proceedings 1986 ACM Conference on LISP and Functional Programming, ACM, New York, Aug. 1986, pp. 351-363.

Digital Library

[9]

HUD^K, P. Collecting interpretations of expressions. Res. Rep. YALEU/DCS/RR-497, Dep. Computer Science, Yale University, New Haven, Conn., 1986.

[10]

HUDAK, P., AND YOUNG, J. Higher order strictness analysis for untyped lambda calculus. In Proceed~ngs of the 12th ACM Symposium on Princzples of Programming Languages (Jan. 1986), pp. 97-109.

Digital Library

[11]

HuG~ES, J. Strictness detection in non-fiat domains. In Lecture Notes in Computer-Sczence, vol. 217: Programs as Data Objects. SpringerWerlag, New York, 1986, pp. 42-62.

Digital Library

[12]

JONES, N.D. Private communications, June 1987.

[13]

JONES, N. D., AND MUCSNICK, S. S. Complexity of fiow analysis, inductive assertion synthesis, and a language due to Dijkstra. In Program Flow Analysis: Theory and Applications. Prentice-Hall, Englewood Cliffs, N. J, 1981, pp. 380-393.

[14]

JONES, N. D., AND M~CROFT, A. Data fiow analysis of applicative programs using minimal function graphs. In Proceedings of the 13th OEymposium on Principles of Programming Languages. ACM, New York, 1986, pp. 296-306

Digital Library

[15]

JONES, N., AND SOND~RGAARD, H. A semantics-based framework for the abstract interpretation of 'Prolog.' In Abstract Interpretation of Declaratwe Languages. Ellis Horwood, Chichester, England, 1987, pp. 123-142.

[16]

LINDS?ROM, G. Statistic evaluation of functional programs. In SIGPLAN '86 Symposium on Compiler Construction. ACM, New York, 1986, pp. 196-206. Published as SIGPLAN Notices 21, 7 (July 1986).

Digital Library

[17]

MELHSS, C. Abstract interpretation of PROLOG programs. In Abstract Interpretation of Declarative Languages. Ellis Horwood, Chichester, England, 1987, pp. 181-198.

[18]

MYCROF% A. Abstract interpretation and optimizing transformations for applicative programs. Ph.D. dissertation, University of Edinburgh, Edinburgh, Scotland, 1981

[19]

M~CROFT, A. The theory and practice of transforming call-by-need into call-by~value. In ProceediT~gs of International Symposium on Programming, Lecture Notes in Computer Science, vol. 83, Springer-Verlag, New York, 1980, pp. 269-281.

Digital Library

[20]

NmLSON, F. Abstract Interpretation Using Domain Theory. Ph.D. dissertation, University of Edinburgh, Edmburgh, Scotland, Oct. 1984.

[21]

NmLSON, F. A denotational framework for data fiow analysis. Acta Inform. 18 (1982), 265-287.

[22]

SCHMIDT, D.A. Denotational Semantics - A Methodology for Language Development. Allyn and Bacon, Boston, Mass., 1986.

Digital Library

[23]

STO~, J. E Denotatwnal Semantics: The Scott-Strachey Approach to Programm~ng Language Theory. M.I.T. Press, Cambridge, Mass, 1977.

Digital Library

[24]

WADLER, P. AND HUGHES, R. J. M. Projections for strictness analysis. In Proceedings of 1987 Funct~onal Programming Languages and Computer Architecture Conference, Lecture Notes in Computer Science, vol. 274. Springer-Verlag, New York, 1987, pp. 385-407.

Digital Library

[25]

YOUNG, J. The semantic analysis of functional programs: Theory and practice. Ph D. dissertation, Dep. Computer Science, Yale Umversity, New Haven, Conn., 1988.

Cited By

Mariano BChen YFeng YDurrett GDillig I(2022)Automated transpilation of imperative to functional code using neural-guided program synthesisProceedings of the ACM on Programming Languages10.1145/35273156:OOPSLA1(1-27)Online publication date: 29-Apr-2022
https://dl.acm.org/doi/10.1145/3527315
Montagu BJensen T(2020)Stable relations and abstract interpretation of higher-order programsProceedings of the ACM on Programming Languages10.1145/34090014:ICFP(1-30)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3409001
Sergey IDevriese DMight MMidtgaard JDarais DClarke DPiessens F(2013)Monadic abstract interpretersACM SIGPLAN Notices10.1145/2499370.249197948:6(399-410)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2499370.2491979
Show More Cited By

Index Terms

Collecting interpretations of expressions
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
    2. General programming languages
      1. Language types
        Functional languages
2. Theory of computation
  1. Formal languages and automata theory
    1. Formalisms
      1. Rewrite systems
    2. Grammars and context-free languages
  2. Semantics and reasoning
    1. Program semantics
      1. Denotational semantics

Recommendations

A collecting interpretation of expressions
POPL '88: Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

A collecting interpretation of expressions is an interpretation of a program that allows one to answer questions of the sort: “What are all possible values to which an expression might evaluate during program execution?” Answering such questions in a ...
Abstract interpretations and abstract machines: contributions to a methodology for the implementation of logic programs
Disunification for ultimately periodic interpretations
LPAR'10: Proceedings of the 16th international conference on Logic for programming, artificial intelligence, and reasoning

Disunification is an extension of unification to first-order formulae over syntactic equality atoms. Instead of considering only syntactic equality, I extend a disunification algorithm by Comon and Delor to ultimately periodic interpretations, i.e. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 13, Issue 2

April 1991

114 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/103135

Editor:
Susan L. Graham
Univ. of California at Berkley

Issue’s Table of Contents

Copyright © 1991 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 April 1991

Published in TOPLAS Volume 13, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tag

theory

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
445
Total Downloads

Downloads (Last 12 months)77
Downloads (Last 6 weeks)20

Reflects downloads up to 13 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Mariano BChen YFeng YDurrett GDillig I(2022)Automated transpilation of imperative to functional code using neural-guided program synthesisProceedings of the ACM on Programming Languages10.1145/35273156:OOPSLA1(1-27)Online publication date: 29-Apr-2022
https://dl.acm.org/doi/10.1145/3527315
Montagu BJensen T(2020)Stable relations and abstract interpretation of higher-order programsProceedings of the ACM on Programming Languages10.1145/34090014:ICFP(1-30)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3409001
Sergey IDevriese DMight MMidtgaard JDarais DClarke DPiessens F(2013)Monadic abstract interpretersACM SIGPLAN Notices10.1145/2499370.249197948:6(399-410)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2499370.2491979
Sergey IDevriese DMight MMidtgaard JDarais DClarke DPiessens FBoehm HFlanagan C(2013)Monadic abstract interpretersProceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2491956.2491979(399-410)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2491956.2491979
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
Colby CLee PBoehm HSteele G(1996)Trace-based program analysisProceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/237721.237776(195-207)Online publication date: 1-Jan-1996
https://dl.acm.org/doi/10.1145/237721.237776
Jagannathan SWeeks SCytron RLee P(1995)A unified treatment of flow analysis in higher-order languagesProceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/199448.199536(393-407)Online publication date: 25-Jan-1995
https://dl.acm.org/doi/10.1145/199448.199536
Sabry AFelleisen M(1994)Is continuation-passing useful for data flow analysis?ACM SIGPLAN Notices10.1145/773473.17824429:6(1-12)Online publication date: 1-Jun-1994
https://dl.acm.org/doi/10.1145/773473.178244
Jagannathan SWeeks S(1994)Analyzing stores and references in a parallel symbolic languageACM SIGPLAN Lisp Pointers10.1145/182590.182493VII:3(294-305)Online publication date: 1-Jul-1994
https://dl.acm.org/doi/10.1145/182590.182493
Jagannathan SWeeks SKessler R(1994)Analyzing stores and references in a parallel symbolic languageProceedings of the 1994 ACM conference on LISP and functional programming10.1145/182409.182493(294-305)Online publication date: 1-Jul-1994
https://dl.acm.org/doi/10.1145/182409.182493
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents