A Dependently Typed Framework for Static Analysis of Program Execution Costs

13 years 10 months ago

Download www.cs.st-andrews.ac.uk

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 deﬁne 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 signiﬁcant 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

Real-time Traffic