TY - GEN
T1 - A coq library for internal verification of running-times
AU - McCarthy, Jay
AU - Fetscher, Burke
AU - New, Max
AU - Feltey, Daniel
AU - Findler, Robert
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2016.
PY - 2016
Y1 - 2016
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84961149731&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84961149731&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-29604-3_10
DO - 10.1007/978-3-319-29604-3_10
M3 - Conference contribution
AN - SCOPUS:84961149731
SN - 9783319296036
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 144
EP - 162
BT - Functional and Logic Programming - 13th International Symposium, FLOPS 2016, Proceedings
A2 - Kiselyov, Oleg
A2 - King, Andy
PB - Springer Verlag
T2 - 13th International Symposium on Functional and Logic Programming, FLOPS 2016
Y2 - 4 March 2016 through 6 March 2016
ER -