Skip to main content
SpringerLink
Log in

Flow Analysis: Games and Nets

  • Chapter
  • First Online:
The Essence of Computation

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2566))

Abstract

This paper presents a graph-based formulation of control- flow analysis using results from game semantics and proof-nets. Control- flow analysis aims to give a conservative prediction of the flow of control in a program. In our analysis, terms are represented by proof-nets and control-flow analysis amounts to the analysis of computation paths in the proof-net. We focus on a context free analysis known in the literature as 0-CFA, and develop an algorithm for the analysis. The algorithm for 0- CFA performs dynamic transitive closure of a graph that is based on the judgement associated with the proof-net. Correctness of the algorithm relies on the correspondence between proof-nets and certain kinds of strategies in game semantics.

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

Access this chapter

Log in via an institution
eBook
USD 16.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. Samson Abramsky, Kohei Honda, and Guy McCusker. A fully abstract game semantics for general references. In Proceedings of LICS’98. IEEE Press, 1998.

    Google Scholar 

  2. Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF (extended abstract). In Proceedings of TACS’94, volume 789 of Lecture Notes in Computer Science, ages 1–15. Springer-Verlag, 1994.

    Google Scholar 

  3. Samson Abramsky and Guy McCusker. Linearity, sharing and state: a fully abstract game semantics for idealized algol with active expressions. In Peter W O’Hearn and R D Tennent, editors, Algol-like Languages, volume 2. Birkhaüser, 1997.

    Google Scholar 

  4. Henk Barendregt, J R Kennaway, J W Klop, and M R Sleep. Needed reduction and spine strategies for the lambda calculus. Information and Computation, 74:191–231, 1987.

    Article  MathSciNet  Google Scholar 

  5. Vincent Danos. Une Application de la Logique Linéaire à l’Étude des Processus de Normalisation (Principalement du Lambda-calcul). PhD thesis, Université Paris VII, 1990.

    Google Scholar 

  6. Alain Deutsch. Modeles Operationnels de Langage de Programmation et Representations de Relations Sur des Langages Rationnels avec Application a la Determination Statique de Proprietes de Partages Dynamiques de Donnees. PhD thesis, Universite Paris VI, 1992.

    Google Scholar 

  7. Vincent Danos, Hugo Herbelin, and Laurent Regnier. Game semantics and abstract machines. In Proceedings of LICS’96. IEEE Press, 1996.

    Google Scholar 

  8. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  9. Russell Harmer. Games and full abstraction for non-deterministic languages. PhD thesis, University of London, 1999.

    Google Scholar 

  10. Nevin Heintze and David McAllester. Linear time subtransitive control flow analysis. In Proceedings of PLDI’97, pages 261–272. ACM SIGPLAN, June 1997.

    Google Scholar 

  11. Nevin Heintze and David McAllester. On the cubic-bottleneck of subtyping and flow analysis. In Proceedings of LICS’97. IEEE Press, 1997.

    Google Scholar 

  12. J. Martin E. Hyland and C.-H L. Ong. On full abstraction for PCF: Parts I, II and III. Available from [Hy 9], 1994.

    Google Scholar 

  13. Neil D Jones. Flow analysis of lambda expressions. In S Even and O Kariv, editors, Proceedings of ICALP’81, number 115 in Lecture Notes in Computer Science, pages 114–128, Acre (Akko), Israel, July 1981. Springer-Verlag.

    Google Scholar 

  14. François Lamarche. Proof nets for intuitionistic linear logic I: Essential nets. Available from [Hy 9], 1994.

    Google Scholar 

  15. François Lamarche. From proof nets to games: extended abstract. ENTCS, 1996.

    Google Scholar 

  16. Ian Mackie. The Geometry of Implementation. PhD thesis, University of London, 1994.

    Google Scholar 

  17. Guy McCusker. Games and Full Abstraction for a Functional Metalanguage with Recursive Types. Distinguished dissertations. Springer-Verlag, 1998.

    Google Scholar 

  18. Pasquale Malacaria and Chris Hankin. Generalised flowcharts and games: Extended abstract. In Kim G Larsen, Sven Skyum, and Glynn Winskel, editors, 25th International Colloquium, ICALP’98, Aalborg, Denmark, July 1998.

    Google Scholar 

  19. Pasquale Malacaria and Chris Hankin. A new approach to control flow analysis. In Koskimies Kai, editor, Proceedings of CC’98, volume 1383 of Lecture Notes in Computer Science, Lisbon, Portugal, 1998. Springer.

    Google Scholar 

  20. Pasquale Malacaria and Chris Hankin. Non-deterministic games and program analysis: An application to security. In Proceedings of LICS’99. IEEE Press, 1999.

    Google Scholar 

  21. Robin Milner. Communication and Concurrency. International series in computer science. Prentice Hall, 1989.

    Google Scholar 

  22. Christian Mossin. Flow Analysis of Typed Higher-Order Programs. PhD thesis, DIKU, University of Copenhagen, 1997.

    Google Scholar 

  23. Christian Mossin. Higher-order value flow graphs. In Proceedings of 9th International Symposium on Programming Languages, Implementation, Logics, and Programming (PLILP’97), 1997.

    Google Scholar 

  24. Gianfranco Mascari and Marco Pedicini. Head linear reduction and pure proof net extraction. In Theoretical Computer Science, volume 135, pages 111–137, 1992.

    Article  MathSciNet  Google Scholar 

  25. Flemming Nielson and Hanne Riis Nielson. Infinitary control flow analysis: A collecting semantics for closure analysis. In Proceedings of POPL’97. ACM Press, 1997.

    Google Scholar 

  26. Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. Principles of Program Analysis. Springer-Verlag, 1999.

    Google Scholar 

  27. Jens Palsberg. Global program analysis in constraint form. In Sophie Tison, editor, Proceedings CAAP’94, volume 787 of Lecture Notes in Computer Science, pages 276–290. Springer-Verlag, 1994.

    Google Scholar 

  28. Prahladavaradan Sampath. On abstract machines and games. In Valeria de Paiva and Eike Ritter, editors, Proceedings of the ESSLLI’98 Workshop on Logical Abstract Machines, Technical Report CSR-98-8. University of Birmingham, 1998.

    Google Scholar 

  29. Prahladavaradan Sampath. Program Analysis using Game Semantics. PhD thesis, University of London, 1999.

    Google Scholar 

  30. Peter Sestoft. Analysis and Efficient Implementation of Functional Programs. PhD thesis, DIKU, Department of Computer Science, University of Copenhagen, 1991.

    Google Scholar 

  31. Olin Shivers. Control-Flow Analysis of Higher-Order Languages (or) Taming Lambda. PhD thesis, School of Computer Science, Carnegie Mellon University, 1991.

    Google Scholar 

  32. C Wadsworth. Semantics and Pragmatics of the Lambda-Calculus. PhD thesis, Oxford University, 1971.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Imperial College of Science, Technology and Medicine, SW7 2BZ, London

    Chris Hankin

  2. University of Warwick, CV4 7AL, Coventry

    Rajagopal Nagarajan

  3. Teamphone.com, W1D 7EQ, London

    Prahladavaradan Sampath

Authors
  1. Chris Hankin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rajagopal Nagarajan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Prahladavaradan Sampath
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. DIKU, University of Copenhagen, Universitetsparken 1, 2100, Copenhagen, Denmark

    Torben Æ. Mogensen

  2. Department of Computing and Information Sciences, Kansas State University, 234 Nichols Hall, 66506, Manhattan, KS, USA

    David A. Schmidt

  3. Department of Computer Science, University of Texas at Dallas, P.O. Box 830688, 75083, Richardson, TX, USA

    I. Hal Sudborough

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Hankin, C., Nagarajan, R., Sampath, P. (2002). Flow Analysis: Games and Nets. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds) The Essence of Computation. Lecture Notes in Computer Science, vol 2566. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36377-7_7

Download citation

  • DOI: https://doi.org/10.1007/3-540-36377-7_7

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00326-7

  • Online ISBN: 978-3-540-36377-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation