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
Publication statusPublished - 2006

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

View graph of relations

Related by author

  1. Value-dependent session design in a dependently typed language

    de Muijnck-Hughes, J., Vanderbauwhede, W. & Brady, E. C., 7 Apr 2019, Electronic Proceedings in Theoretical Computer Science. Open Publishing Association

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

  2. Subtype polymorphism à la carte via machine learning on dependent types

    Swan, J., Johnson, C. G. & Brady, E. C., 16 Jul 2018, Companion Proceedings for the ISSTA/ECOOP 2018 Workshops. New York, NY: Association for Computing Machinery, Inc, p. 14-16 3 p.

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

  3. Type driven development of concurrent communicating systems

    Brady, E. C., 7 Jul 2017, In : Computer Science. 18, 3, 22 p., 1413.

    Research output: Contribution to journalArticle

  4. Sequential decision problems, dependent types and generic solutions

    Botta, N., Jansson, P., Ionescu, C., Christiansen, D. & Brady, E. C., 17 Mar 2017, In : Logical Methods in Computer Science. 13, 1, 23 p., 7.

    Research output: Contribution to journalArticle

  5. Type-driven development with Idris

    Brady, E. C., Mar 2017, Shelter Island: Manning Publications Co. 480 p.

    Research output: Book/ReportBook

ID: 64171855