A Verified Resource-Bounded Functional Programming Language
Edwin C. Brady, Kevin L Hammond, James McKinna · 2006
This paper studies the problem of constructing formal bounds on program resource usage and other complex properties using fullspectrum dependent types to encode resource usage properties over size information and the associated correctness proofs as program terms in a simple resource-aware functional language, . Since resource properties and the associated proofs are directly expressed in through strong program structures associated with a formal program logic, it follows that correctly specified resource properties of programs written in our language can be formally and automatically verified simply by composing proofs according to the underlying program structure. We illustrate this by constructing a dependently typed interpreter for that ensures that the representation of terms includes explicit and independently checkableproofs that the required resource properties are satisfied. In this way we are able to construct programs with strong upper bounds on resource usage that can be formally and automatically verified. Compared with other automatic approaches to bounding resource usage, our work has the twin advantages of flexibility and generality, whilst retaining simplicity and automation. This is achieved through the use of full-spectrum dependent types rather than the more simply typed approaches in previous use. We illustrate the advantages of the approach by considering some complex operations on lists and trees.