Embedding a Language with Certified Size Constraints in a Dependently Typed Metalanguage
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. We use fullspectrum dependent types to embed a language of terms, RAFL, with resource usage properties and associated correctness proofs. Since these properties and associated proofs are directly expressed in RAFL through a formal logic, it follows that correctly specified resource properties of programs written in RAFL can be formally verified simply by composing proofs according to the underlying program structure. We illustrate this by constructing a dependently typed interpreter for RAFL that ensures that the representation of RAFLterms includesexplicit andindependently checkableproofs that the required resource properties are satisfied. In this way we are able to construct programs with strong bounds on resource usage that can be automatically checked. Compared with other approaches to bounding resource usage, our work has the twin advantages of flexibility and generality, whilst retaining simplicity and automation. We demonstrate these advantages by considering some representative operations on lists and trees.