A coq library for internal verification of running-times

Jay McCarthy*, Burke Fetscher, Max New, Daniel Feltey, Robert Findler

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationFunctional and Logic Programming - 13th International Symposium, FLOPS 2016, Proceedings
EditorsOleg Kiselyov, Andy King
PublisherSpringer Verlag
Pages144-162
Number of pages19
ISBN (Print)9783319296036
DOIs
StatePublished - Jan 1 2016
Event13th International Symposium on Functional and Logic Programming, FLOPS 2016 - Kochi, Japan
Duration: Mar 4 2016Mar 6 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9613
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other13th International Symposium on Functional and Logic Programming, FLOPS 2016
CountryJapan
CityKochi
Period3/4/163/6/16

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A coq library for internal verification of running-times'. Together they form a unique fingerprint.

  • Cite this

    McCarthy, J., Fetscher, B., New, M., Feltey, D., & Findler, R. (2016). A coq library for internal verification of running-times. In O. Kiselyov, & A. King (Eds.), Functional and Logic Programming - 13th International Symposium, FLOPS 2016, Proceedings (pp. 144-162). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9613). Springer Verlag. https://doi.org/10.1007/978-3-319-29604-3_10