This paper presents a Coq library that lifts an abstract yet precise notion of running-time into the type of a function. Our library is based on a monad that counts abstract steps, controlled by one of the monadic operations. The monad’s computational content, however, is simply that of the identity monad so programs written in our monad (that recur on the natural structure of their arguments) extract into idiomatic OCaml code. We evaluated the expressiveness of the library by proving that red-black tree insertion and search, merge sort, insertion sort, Fibonacci, iterated list insertion, BigNum addition, and Okasaki’s Braun Tree algorithms all have their expected running times.
CITATION STYLE
McCarthy, J., Fetscher, B., New, M., Feltey, D., & Findler, R. B. (2016). A coq library for internal verification of running-times. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9613, pp. 144–162). Springer Verlag. https://doi.org/10.1007/978-3-319-29604-3_10
Mendeley helps you to discover research relevant for your work.