A dependently typed framework for static analysis of program execution costs

E. Brady, Kevin Hammond

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

13 Citations (Scopus)

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

Fingerprint

Dive into the research topics of 'A dependently typed framework for static analysis of program execution costs'. Together they form a unique fingerprint.

Cite this