Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

PERs from projections for binding-time analysis

  • Published:
LISP and Symbolic Computation

Abstract

First-order projection-based binding-time analysis has proven genuinely useful in partial evaluation [18]. There have been three notable generalisations of projection-based analysis to higher order. The first lacked a formal basis [19]; the second used structures strictly more general than projections, namelypartial equivalence relations (PERs) [14]; the third involved a complex construction that gave rise to impractically large abstract domains [7]. This paper presents a technique free of these shortcomings: it is simple, entirely projection-based, satisfies a formal correctness condition, and gives rise to reasonably small abstract domains. Though the technique is cast in terms of projections, there is also an interpretation in terms of PERs. The principal limitation of the technique is the restriction tomonomorphic typing.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. S. Abramsky. The lazy lambda calculus. In D. Turner, editor,Research Topics in Functional Programming. Addison-Wesley, 1989.

  2. S. Abramsky. Abstract interpretation, logical relations and Kan extensions.Journal of Logic and Computation, 1, 1990.

  3. G. Baraki. A note on abstract interpretation of polymorphic functions. In [12], pages 367–378.

  4. G. Baraki.Abstract Interpretation of Polymorphic Higher-Order Functions. Ph.D. thesis, Research report FP-1993-7, Department of Computing Science, University of Glasgow, 1993.

  5. D. Bjørner, A.P. Ershov, and N.D. Jones, editors,Partial Evaluation and Mixed Computation, Proceedings IFIP TC2 Workshop. North-Holland, 1988.

  6. C. Consel. Binding time analysis for higher order untyped functional languages.1990 ACM Conference on LISP and Functional Programming, pages 264–272. ACM Press, 1990.

  7. K. Davis. Higher-order binding-time analysis.ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'93), pages 78–87. ACM Press, 1993.

  8. K. Davis.Projection-Based Program Analysis. Ph.D. thesis, Computing Science Department, University of Glasgow, 1994.

  9. C.K. Gomard. A self-applicable partial evaluator for the lambda calculus: Correctness and pragmatics. ACM Transactions on Programming Languages and Systems, 14(2):147–172, 1992.

    Google Scholar 

  10. F. Henglein and C. Mossin. Polymorphic binding-time analysis. In D. Sannella, editor,Programming Languages and Systems — ESOP'94. 5th European Symposium on Programming. LNCS 788, pages 287–301. Springer-Verlag, 1994.

  11. J. Hughes. Backwards analysis of functional programs. In [5], pages 187–208.

  12. J. Hughes, editor,Proceedings of the 1991 Conference on Functional Programming Languages and Computer Architecture (FPCA '91), LNCS 523. Springer-Verlag, 1991.

  13. S. Hunt. PERs generalise projections for strictness analysis (extended abstract). In S.L. Peyton Joneset al., editors,Proceedings of the 1990 Glasgow Workshop on Functional Programming. Springer-Verlag, 1991.

  14. S. Hunt and D. Sands. Binding time analysis: A new PERspective.ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'91), SIGPLAN Notices 26(9):154–165, 1991.

    Google Scholar 

  15. T. Jensen.Abstract Interpretation in Logical Form. Ph.D. thesis, Report 93/11, Department of Computer Science, University of Copenhagen, 1992.

  16. N.D. Jones. Automatic program specialization: A re-examination from basic principles. In [5], pages 225–282.

  17. J. Launchbury. Projections for specialisation. In [5], pages 299–315.

  18. J. Launchbury.Projection Factorisations in Partial Evaluation. Ph.D. Thesis, Glasgow University, 1989. Distinguished Dissertations in Computer Science, vol. 1, Cambridge University Press, 1991.

  19. T. Mogensen. Binding-time analysis for polymorphically typed higher order languages. In J. Diaz and F. Orejas, editors,International Joint Conference on Theory and Practice of Software Development, LNCS 352, pages 298–312. Springer-Verlag, 1989.

  20. H.R. Nielson and F. Nielson. Automatic binding-time analysis for a typed λ-calculus.Science of Computer Programming 10:139–176.

  21. D.A. Schmidt. Static properties of partial reduction. In [5], pages 465–483.

  22. J. Seward. Polymorphic strictness analysis using frontiers.ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '93), pages 139–176. ACM Press, 1993.

  23. P. Wadler. Strictness analysis on non-flat domains by abstract interpretation over finite domains. In S. Abramsky and C. Hankin, editors,Abstract Interpretation of Declarative Languages, pages 266–275. Ellis Horwood, 1987.

Download references

Author information

Authors and Affiliations

  1. Los Alamos National Laboratory, MS 8258, 87545, Los Alamos, NM, USA

    Kei Davis

Authors
  1. Kei Davis
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Davis, K. PERs from projections for binding-time analysis. Lisp and Symbolic Computation 8, 249–266 (1995). https://doi.org/10.1007/BF01019006

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF01019006

Keywords

Search

Navigation