Sciweavers

Share
IFL
2005
Springer

A Dependently Typed Framework for Static Analysis of Program Execution Costs

9 years 21 days ago
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. 1 Background and Motivation Obtaining accurate information about the run-time time and space behaviour of computer software is important in a number of areas. One of the most significant of these is embedded systems. Embedded systems are becoming an increasingly important application area: today, more than 98% of all processors are used i...
Edwin Brady, Kevin Hammond
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Where IFL
Authors Edwin Brady, Kevin Hammond
Comments (0)
books