A dependently typed framework for static analysis of program execution costs

E. Brady; Kevin Hammond

doi:10.1007/11964681_5

A dependently typed framework for static analysis of program execution costs

E. Brady, Kevin Hammond

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 language	English
Title of host publication	Implementation and Application of Functional Languages
Subtitle of host publication	17th International Workshop, IFL 2005, Dublin, Ireland, September 19-21, 2005, Revised Selected Papers
Editors	Andrew Butterfield, Clemens Grelck, Frank Huch
Place of Publication	Berlin
Publisher	Springer
Pages	74-90
Volume	4105
ISBN (Electronic)	978-3-540-69175-4
ISBN (Print)	978-3-540-69174-7
DOIs	https://doi.org/10.1007/11964681_5
Publication status	Published - 2006

Access to Document

10.1007/11964681_5

EP/C001346/1: Generative Programming for Embedded Systems
Hammond, K. (PI)
EPSRC
1/01/05 → 31/12/07
Project: Standard

Cite this

Brady, E., & Hammond, K. (2006). A dependently typed framework for static analysis of program execution costs. In A. Butterfield, C. Grelck, & F. Huch (Eds.), Implementation and Application of Functional Languages: 17th International Workshop, IFL 2005, Dublin, Ireland, September 19-21, 2005, Revised Selected Papers (Vol. 4105, pp. 74-90). Springer. https://doi.org/10.1007/11964681_5

Brady, E. ; Hammond, Kevin. / A dependently typed framework for static analysis of program execution costs. Implementation and Application of Functional Languages: 17th International Workshop, IFL 2005, Dublin, Ireland, September 19-21, 2005, Revised Selected Papers. editor / Andrew Butterfield ; Clemens Grelck ; Frank Huch. Vol. 4105 Berlin : Springer, 2006. pp. 74-90

@inproceedings{962107aaae3744ddad1643d5d60fb523,

title = "A dependently typed framework for static analysis of program execution costs",

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

author = "E. Brady and Kevin Hammond",

year = "2006",

doi = "10.1007/11964681_5",

language = "English",

isbn = "978-3-540-69174-7",

volume = "4105",

pages = "74--90",

editor = "Andrew Butterfield and Grelck, {Clemens } and Frank Huch",

booktitle = "Implementation and Application of Functional Languages",

publisher = "Springer",

address = "Netherlands",

}

Brady, E & Hammond, K 2006, A dependently typed framework for static analysis of program execution costs. in A Butterfield, C Grelck & F Huch (eds), Implementation and Application of Functional Languages: 17th International Workshop, IFL 2005, Dublin, Ireland, September 19-21, 2005, Revised Selected Papers. vol. 4105, Springer, Berlin, pp. 74-90. https://doi.org/10.1007/11964681_5

A dependently typed framework for static analysis of program execution costs. / Brady, E.; Hammond, Kevin.
Implementation and Application of Functional Languages: 17th International Workshop, IFL 2005, Dublin, Ireland, September 19-21, 2005, Revised Selected Papers. ed. / Andrew Butterfield; Clemens Grelck; Frank Huch. Vol. 4105 Berlin: Springer, 2006. p. 74-90.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - A dependently typed framework for static analysis of program execution costs

AU - Brady, E.

AU - Hammond, Kevin

PY - 2006

Y1 - 2006

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

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

U2 - 10.1007/11964681_5

DO - 10.1007/11964681_5

M3 - Conference contribution

SN - 978-3-540-69174-7

VL - 4105

SP - 74

EP - 90

BT - Implementation and Application of Functional Languages

A2 - Butterfield, Andrew

A2 - Grelck, Clemens

A2 - Huch, Frank

PB - Springer

CY - Berlin

ER -

Brady E, Hammond K. A dependently typed framework for static analysis of program execution costs. In Butterfield A, Grelck C, Huch F, editors, Implementation and Application of Functional Languages: 17th International Workshop, IFL 2005, Dublin, Ireland, September 19-21, 2005, Revised Selected Papers. Vol. 4105. Berlin: Springer. 2006. p. 74-90 doi: 10.1007/11964681_5

A dependently typed framework for static analysis of program execution costs

Abstract

Access to Document

Fingerprint

Projects

EP/C001346/1: Generative Programming for Embedded Systems

Cite this