Skip to main content
SpringerLink
Log in

The Abstract Interpretation of Functional Languages

  • Conference paper
Theory and Formal Methods 1993

Part of the book series: Workshops in Computing ((WORKSHOPS COMP.))

  • 68 Accesses

Abstract

Abstract interpretation is a methodology for developing provably correct program analyses. Uses of such analyses include optimising compilers and program verification.

In this introductory paper, we introduce key issues in the abstract interpretation of higher-order languages, including some open problems. Intuitions, examples and open problems are given instead of a list of theorems.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. Abramsky. Abstract interpretation, logical relations and Kan extensions. Journal of Logic and Computation, 1 (1): 5–39, 1990.

    Article  MathSciNet  Google Scholar 

  2. S. Abramsky and T.P. Jensen. A relational approach to strictness analysis for higher-order functions. In Proceedings of the Symposium on Principles of Programming Languages, pages 49–54, Orlando, Florida, 21–23 January 1991.

    Google Scholar 

  3. A.V. Aho, R. Sethi, and J.D. Ullman. Compilers: Principles, Techniques and Tools. Addison-Wesley, Reading, MA, 1986.

    Google Scholar 

  4. G. Baraki. Abstract Interpretation of Polymorphic Higher-Order Functions. PhD thesis, Department of Computer Science, University of Glasgow, Lilybank Gardens, Glasgow G12 SQQ, UK, 1993.

    Google Scholar 

  5. P.N. Benton. Strictness logic and polymorphic invariance. In A. Nerode and M. Taitslin, editors, Proceedings of the International Symposium on Logical Foundations of Computer Science,pages 33–44, Tver, Russia, 20–24 July 1992. Springer-Verlag LNCS620.

    Google Scholar 

  6. G.L. Burn. Lazy Functional Languages: Abstract Interpretation and Compilation. Research Monographs in Parallel and Distributed Computing. Pitman in association with MIT Press, 1991. 238 pp.

    MATH  Google Scholar 

  7. G.L. Burn. A logical framework for program analysis. In J. Launchbury and P. Sansom, editors, Proceedings of the 1992 Glasgow Functional Programming Workshop, pages 3042. Springer-Verlag Workshops in Computer Science series, 6–8 July 1992.

    Google Scholar 

  8. G.L. Burn. Properties of progam analysis techniques. Technical Report DOC92/19, Imperial College of Science, Technology and Medicine, Department of Computing, June 1992.

    Google Scholar 

  9. C. Clack and S.L. Peyton Jones. Strictness analysis — a practical approach. In J.-P. Jouannaud, editor, Proceedings of the Functional Programming Languages and Computer Architecture Conference, pages 35–49. Springer-Verlag LNCS 201, September1985.

    Google Scholar 

  10. P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming, 13 (2–3): 103–179, 1992.

    Article  MathSciNet  MATH  Google Scholar 

  11. P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In M. Bruynooghe and M. Wirsing, editors, Programming Language Implementation and Logic Programming, Proceedings of the Fourth International Symposium, pages 269–295. Springer-Verlag LNCS631, Leuven, Belgium, August 1992.

    Google Scholar 

  12. P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In POPL’92, pages 83–95. ACM, Albuquerque, New Mexico, 19–22 January 1992.

    Google Scholar 

  13. A. Deutsch. An operational model of strictness properties and its abstractions (extended abstract). In R. Heldal, C. Kehler Holst, and P. Wadler, editors, Proceedings of the 1991 Glasgow Functional Programming Workshop, 13–15 August 1991.

    Google Scholar 

  14. C. Ernoult and A. Mycroft. Uniform ideals and strictness analysis. In Proceedings of ICALP’91. Springer-Verlag Lecture Notes in Computer Science, 1991.

    Google Scholar 

  15. A.B. Ferguson and R.J.M. Huges. Abstract interpretation of higher-order functions using concrete data structures (summary). In J. Launchbury and P. Sansom, editors, Proceedings of the 1992 Glasgow Functional Programming Workshop, pages 57–61. Springer-Verlag Workshops in Computer Science series, 6–8 July 1992.

    Google Scholar 

  16. P. Granger. Combinations of semantic analyses. In INRIA, editor, Proceedings of Informatika 88 (French-Soviet Workshop), pages 71–88, Nice, February 1988.

    Google Scholar 

  17. C.V. Hall and D.S. Wise. Generating function versions using rational strictness patters. Science of Computer Programming, 12: 39–74, 1989.

    Article  MathSciNet  MATH  Google Scholar 

  18. Chris Hankin and Sebastian Hunt. Approximate fixed points in abstract interpretation. In B. Krieg-Brückner, editor, ESOP’92, pages 219–232. Springer-Verlag LNCS 582, 1992.

    Google Scholar 

  19. S. Holmström. Polymorphic Type Systems and Concurrent Computation in Functional Languages. PhD thesis, Chalmers Tekniska Högskola, Göteborg, Sweden, 1983.

    Google Scholar 

  20. L.S. Hunt. Abstract Interpretation of Functional Languages: From Theory to Practice. PhD thesis, Department of Computing, Imperial College of Science, Technology and Medicine, University of London, 1991.

    Google Scholar 

  21. L.S. Hunt and D. Sands. Binding time analysis: A new PERspective. In Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM’91),pages 154–165, Yale University, USA, 11–19 June 1991. ACM.

    Google Scholar 

  22. T. P. Jensen. Abstract Interpretation in Logical Form. PhD thesis, Imperial College, University of London, November 1992.

    Google Scholar 

  23. S. Kamin. Head-strictness is not a monotonic abstract property. Information Processing Letters,1991. To appear.

    Google Scholar 

  24. C. Martin and C. Hankin. Finding fixed points in finite lattices. In G. Kahn, editor, Proceedings of the Functional Programming Languages and Computer Architecture Conference, pages 426–445. Springer-Verlag LNCS 274, September 1987.

    Google Scholar 

  25. B. Monsuez. Type inference by abstract interpretation. Technical report, Laboratoire d’informatique de l’École Polytechnique, 91128 Palaiseau Cedex, France, February 1991.

    Google Scholar 

  26. S.S. Muchnick and N.D. Jones, editors. Program Flow Analysis: Theory and Applications. Prentice–Hall Software Series. Prentice–Hall, 1981. ISBN 0–13–729681–9.

    Google Scholar 

  27. J. Muylaert Filho and G.L. Burn. Continuation passing transformation and abstract intrepretation. In this volume.

    Google Scholar 

  28. F. Nielson. Tensor products generalise the relational data flow analysis method. In Proceedings of the 4th Hungarian Computer Science Conference, pages 211–225, 1985.

    Google Scholar 

  29. F. Nielson. Two-level semantics and abstract interpretation. Theoretical Computer Science, 69: 117–242, 1989.

    Article  MathSciNet  MATH  Google Scholar 

  30. F. Nielson and H. Riffs Nielson. The tensor product in Wadler’s analysis of lists. In B. Krieg-Bruckner, editor, Proceedings of ESOP’92, pages 351–370, Rennes, France, February 1992. Springer-Verlag LNCS582. Preliminary version of Chapter 8 of Two-level Functional Languages, CUP, 1992.

    Google Scholar 

  31. P. Wadler and R. J. M. Hughes. Projections for strictness analysis. In G. Kahn, editor, Proceedings of the Functional Programming Languages and Computer Architecture Conference, pages 385–407. Springer-Verlag LNCS 274, September 1987.

    Google Scholar 

  32. P.L. Wadler. Strictness analysis on non-flat domains (by abstract interpretation over finite domains). In S. Abramsky and C.L. Hankin, editors, Abstract Interpretation of Declarative Languages, chapter 12, pages 266–275. Ellis Horwood Ltd., Chichester, West Sussex, England, 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing, Imperial College, 180 Queen’s Gate, London, SW7 2BZ, UK

    Geoffrey Burn

Authors
  1. Geoffrey Burn
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing, Imperial College of Science, Technology and Medicine, 180 Queen’s Gate, SW7 2BZ, London, UK

    Geoffrey Burn BSc (Hons), PhD, DIC , Simon Gay BA (Hons), DipCompSci  & Mark Ryan MA, PhD ,  & 

Rights and permissions

Reprints and permissions

Copyright information

© 1993 British Computer Society

About this paper

Cite this paper

Burn, G. (1993). The Abstract Interpretation of Functional Languages. In: Burn, G., Gay, S., Ryan, M. (eds) Theory and Formal Methods 1993. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3503-6_1

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-3503-6_1

  • Publisher Name: Springer, London

  • Print ISBN: 978-3-540-19842-0

  • Online ISBN: 978-1-4471-3503-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation