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

• Type: Conference
• Year: 2005
• Where: IFL
• Authors: Edwin Brady, Kevin Hammond
• Keywords: Dependent Types, Embedded Software, Embedded Systems, IFL 2005