Skip to main content
SpringerLink
Log in
Book cover

Symposium on Implementation and Application of Functional Languages

IFL 2005: Implementation and Application of Functional Languages pp 74–90Cite as

A Dependently Typed Framework for Static Analysis of Program Execution Costs

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4015))

Abstract

This paper considers the use of dependent types to capture information about dynamic resource usage in a static type system. Dependent types allow us to give (explicit) proofs of properties with a program; we present a dependently typed core language TT, and define a framework within this language for representing size metrics and their properties. We give several examples of size bounded programs within this framework and show that we can construct proofs of their size bounds within TT. We further show how the framework handles recursive higher order functions and sum types, and contrast our system with previous work based on sized types.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Altenkirch, T., McBride, C., McKinna, J.: Why dependent types matter (2005) (submitted for publication)

    Google Scholar 

  2. Augustsson, L.: Cayenne — a language with dependent types. In: Proc. ACM SIGPLAN International Conf. on Functional Programming (ICFP 1998). ACM SIGPLAN Notices, vol. 34(1), pp. 239–250. ACM, New York (1999)

    Google Scholar 

  3. Augustsson, L., Carlsson, M.: An exercise in dependent types: A well-typed interpreter (1999)

    Google Scholar 

  4. Brady, E.: Practical Implementation of a Dependently Typed Functional Programming Language. PhD thesis, University of Durham (2005)

    Google Scholar 

  5. Burstall, R.: Inductively Defined Functions in Functional Programming Languages. Technical Report ECS-LFCS-87-25, Dept. of Comp. Sci., Univ. of Edinburgh (April 1987)

    Google Scholar 

  6. Coq Development Team. The Coq proof assistant — reference manual (2004), http://coq.inria.fr/

  7. Crary, K., Weirich, S.: Resource bound certification. In: The Symposium on Principles of Programming Languages (POPL 2000), January  19–21, 2000, pp. 184–198. ACM Press, New York (2000)

    Chapter  Google Scholar 

  8. Curry, H.B., Feys, R.: Combinatory Logic, vol. 1. North-Holland, Amsterdam (1958)

    MATH  Google Scholar 

  9. Dybjer, P.: Inductive families. Formal Aspects of Computing 6(4), 440–465 (1994)

    Article  MATH  Google Scholar 

  10. Grobauer, B.: Topics in Semantics-based Program Manipluation. PhD thesis, BRICS, Department of Computer Science, University of Aarhus (August 2001)

    Google Scholar 

  11. Hammond, K., Michaelson, G.J.: Hume: A Domain-Specific Language for Real-Time Embedded Systems. In: Pfenning, F., Smaragdakis, Y. (eds.) GPCE 2003. LNCS, vol. 2830, pp. 37–56. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  12. Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: Proc. POPL 2003 — 2003 ACM Symp. on Principles of Programming Languages, pp. 185–197. ACM Press, New York (2003)

    Google Scholar 

  13. Howard, W.A.: The formulae-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B.Curry: Essays on combinatory logic, lambda calculus and formalism. Academic Press, London (1980); A reprint of an unpublished manuscript from 1969

    Google Scholar 

  14. Hughes, R., Pareto, L.: Recursion and Dynamic Data Structures in Bounded Space: Towards Embedded ML Programming. In: Proc. 1999 ACM Intl. Conf. on Functional Programming (ICFP 1999), pp. 70–81 (1999)

    Google Scholar 

  15. Hughes, R., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: Proc. ACM Symp. on Principles of Prog. Langs. (POPL 1996). ACM Press, New York (1996)

    Google Scholar 

  16. Luo, Z.: Computation and Reasoning – A Type Theory for Computer Science. International Series of Monographs on Computer Science. OUP (1994)

    Google Scholar 

  17. Luo, Z., Pollack, R.: LEGO proof development system: User’s manual. Technical report, Department of Computer Science, University of Edinburgh (1992)

    Google Scholar 

  18. McBride, C.: Dependently Typed Functional Programs and their proofs. PhD thesis, University of Edinburgh (May 2000)

    Google Scholar 

  19. McBride, C.: Epigram: Practical programming with dependent types. In: Vene, V., Uustalu, T. (eds.) AFP 2004. LNCS, vol. 3622, pp. 130–170. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  20. McBride, C., McKinna, J.: The view from the left. Journal of Functional Programming 14(1), 69–111 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  21. Morris, P., Altenkirch, T., McBride, C.: Exploring the regular tree types. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 252–267. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  22. Mycroft, A., Sharp, R.: A statically allocated parallel functional language. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 37–48. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  23. Pugh, W.: The Omega Test: a fast and practical integer programming algorithm for dependence analysis. Communication of the ACM, pp. 102–114 (1992)

    Google Scholar 

  24. Rebón Portillo, A., Hammond, K., Loidl, H.-W., Vasconcelos, P.: A Sized Time System for a Parallel Functional Language (Revised). In: Peña, R., Arts, T. (eds.) IFL 2002. LNCS, vol. 2670, Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  25. Tofte, M., Talpin, J.-P.: Region-based memory management. Information and Computation 132(2), 109–176 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  26. Turner, D.A.: Elementary Strong Functional Programming. In: Hartel, P.H., Plasmeijer, R. (eds.) FPLE 1995. LNCS, vol. 1022, Springer, Heidelberg (1995)

    Google Scholar 

  27. Wan, Z., Taha, W., Hudak, P.: Real-time FRP. In: Proc. Intl. Conf. on Functional Programming (ICFP 2001), Florence, Italy. ACM, New York (2001)

    Google Scholar 

  28. Wan, Z., Taha, W., Hudak, P.: Event-driven FRP. In: Proc. 4th. Intl. Sym. on Practical Aspects of Declarative Languages (PADL 2002). ACM, New York (2002)

    Google Scholar 

  29. Xi, H., Pfenning, F.: Eliminating array bound checking through dependent types. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, Montreal, pp. 249–257 (June 1998)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, University of St Andrews, St Andrews, Scotland

    Edwin Brady & Kevin Hammond

Authors
  1. Edwin Brady
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kevin Hammond
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Trinity College Dublin, Ireland

    Andrew Butterfield

  2. University of Lübeck, Germany

    Clemens Grelck

  3. Institute of Computer Science, University of Kiel, 24098, Kiel, Germany

    Frank Huch

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Brady, E., Hammond, K. (2006). A Dependently Typed Framework for Static Analysis of Program Execution Costs. In: Butterfield, A., Grelck, C., Huch, F. (eds) Implementation and Application of Functional Languages. IFL 2005. Lecture Notes in Computer Science, vol 4015. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11964681_5

Download citation

  • DOI: https://doi.org/10.1007/11964681_5

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation