Skip to main content
SpringerLink
Log in

Global and Local Space Properties of Stream Programs

  • Conference paper
Foundational and Practical Aspects of Resource Analysis (FOPARA 2009)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6324))

  • 205 Accesses

Abstract

In this paper, we push forward the approach proposed in [1] aiming at studying semantic interpretation criteria for the purpose of ensuring safety and complexity properties of programs working on streams. The paper improves the previous results by considering global and local upper bounds properties of both theoretical and practical interests guaranteeing that the size of each output stream element is bounded by a function in the maximal size of the input stream elements. Moreover, in contrast to previous studies, these properties also apply to a wide class of stream definitions, that is functions that do not have streams in the input but produce an output stream.

Work partially supported by the projects ANR-08-BLANC-0211-01 “COMPLICE”, MIUR-PRIN’07 “CONCERTO” and INRIA Associated Team CRISTAL.

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. Gaboardi, M., Péchoux, R.: Upper bounds on stream I/O using semantic interpretations. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 271–286. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  2. Kennaway, J., Klop, J., Sleep, M., de Vries, F.: Transfinite Reductions in Orthogonal Term Rewriting Systems. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 1–12. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  3. Kennaway, J., Klop, J., Sleep, M., de Vries, F.: Infinitary lambda calculus. TCS 175(1), 93–125 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  4. Weihrauch, K.: A foundation for computable analysis. In: Freksa, C., Jantzen, M., Valk, R. (eds.) Foundations of Computer Science. LNCS, vol. 1337, pp. 185–199. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  5. Henderson, P., Morris, J.: A lazy evaluator. In: POPL’76, pp. 95–103. ACM, New York (1976)

    Google Scholar 

  6. Pitts, A.M.: Operationally-based theories of program equivalence. In: Semantics and Logics of Computation. Cambridge University Press, Cambridge (1997)

    Chapter  Google Scholar 

  7. Gordon, A.: Bisimilarity as a theory of functional programming. TCS 228(1-2), 5–47 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  8. Dijkstra, E.W.: On the productivity of recursive definitions. EWD 749 (1980)

    Google Scholar 

  9. Sijtsma, B.: On the productivity of recursive list definitions. ACM TOPLAS 11(4), 633–649 (1989)

    Article  Google Scholar 

  10. Coquand, T.: Infinite objects in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 62–78. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  11. Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: POPL’96, pp. 410–423. ACM, New York (1996)

    Google Scholar 

  12. Buchholz, W.: A term calculus for (co-) recursive definitions on streamlike data structures. Annals of Pure and Applied Logic 136(1-2), 75–90 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  13. Endrullis, J., Grabmayer, C., Hendriks, D., Isihara, A., Klop, J.: Productivity of Stream Definitions. In: Csuhaj-Varjú, E., Ésik, Z. (eds.) FCT 2007. LNCS, vol. 4639, pp. 274–287. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  14. Frankau, S., Mycroft, A.: Stream processing hardware from functional language specifications. In: HICSS 2003, pp. 278–287. IEEE, Los Alamitos (2003)

    Google Scholar 

  15. Shkaravska, O., van Eekelen, M., Tamalet, A.: Collected Size Semantics for Functional Programs over Polymorphic Nested Lists. Technical Report ICIS–R09003, Radboud University Nijmegen (2009)

    Google Scholar 

  16. Burrell, M.J., Cockett, R., Redmond, B.F.: Pola: a language for PTIME programming. In: LCC 2009, LICS Workshop (2009)

    Google Scholar 

  17. Bonfante, G., Marion, J.Y., Moyen, J.Y.: Quasi-interpretations, a way to control resources. TCS - Accepted

    Google Scholar 

  18. Marion, J.Y., Péchoux, R.: Resource analysis by sup-interpretation. In: Hagiya, M., Wadler, P. (eds.) FLOPS 2006. LNCS, vol. 3945, pp. 163–176. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  19. Amadio, R.: Synthesis of max-plus quasi-interpretations. Fundamenta Informaticae 65(1-2), 29–60 (2005)

    MathSciNet  MATH  Google Scholar 

  20. Bonfante, G., Marion, J.Y., Moyen, J.Y., Péchoux, R.: Synthesis of quasi-interpretations. In: LCC 2005, LICS Workshop (2005), http://hal.inria.fr/

  21. Marion, J.Y., Péchoux, R.: Characterizations of polynomial complexity classes with a better intensionality. In: PPDP’08, pp. 79–88. ACM, New York (2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Scienze dell’Informazione, Università di Bologna, Italy

    Marco Gaboardi

  2. Université Nancy 2, Nancy-université & INRIA project Carte, Loria

    Romain Péchoux

Authors
  1. Marco Gaboardi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Romain Péchoux
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute for Computing and Information Sciences, Radboud Universiteit Nijmegen, P.O. Box 9102, 6500 HC, Nijmegen, The Netherlands

    Marko van Eekelen

  2. Institute for Computing and Information Sciences, Radboud University Nijmegen, The Netherlands

    Olha Shkaravska

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gaboardi, M., Péchoux, R. (2010). Global and Local Space Properties of Stream Programs. In: van Eekelen, M., Shkaravska, O. (eds) Foundational and Practical Aspects of Resource Analysis. FOPARA 2009. Lecture Notes in Computer Science, vol 6324. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15331-0_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15331-0_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-15330-3

  • Online ISBN: 978-3-642-15331-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation