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

10 Scopus citations


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
Number of pages19
ISBN (Print)9783319296036
StatePublished - 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)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other13th International Symposium on Functional and Logic Programming, FLOPS 2016

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


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

Cite this