Skip to content

Research at St Andrews

A dependently typed framework for static analysis of program execution costs

Research output: Chapter in Book/Report/Conference proceedingConference contribution

DOI

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.
Close

Details

Original languageEnglish
Title of host publicationImplementation and Application of Functional Languages
Subtitle of host publication17th International Workshop, IFL 2005, Dublin, Ireland, September 19-21, 2005, Revised Selected Papers
EditorsAndrew Butterfield, Clemens Grelck, Frank Huch
Place of PublicationBerlin
PublisherSpringer
Pages74-90
Volume4105
ISBN (Electronic)978-3-540-69175-4
ISBN (Print)978-3-540-69174-7
DOIs
StatePublished - 2006

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Resource-Safe Systems Programming with Embedded Domain Specific Languages

    Brady, E. C. & Hammond, K. 2012 Practical Aspects of Declarative Languages: 14th International Symposium, PADL 2012, Philadelphia, PA, USA, January 23-24, 2012. Proceedings. Russo, C. & Zhou, N-F. (eds.). Springer, Vol. 7149, p. 242-257 16 p. (Lecture Notes in Computer Science)

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  2. Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation

    Brady, E. C. & Hammond, K. 2010 ICFP '10: Proceedings of the 15th ACM SIGPLAN international conference on Functional programming. ACM, p. 297-308 12 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  3. Lightweight Invariants with Full Dependent Types

    Brady, E. C., Herrmann, C. A. & Hammond, K. 2008 Trends in Functional Programming. Intellect Books

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

ID: 64171855