A Coq library for internal verification of running-times

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

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

5 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. 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, various Fibonacci number implementations, iterated list insertion, various BigNum operations, and Okasaki's Braun Tree algorithms all have their expected running times.

Original languageEnglish (US)
Pages (from-to)49-65
Number of pages17
JournalScience of Computer Programming
Volume164
DOIs
StatePublished - Oct 15 2018

Keywords

  • Complexity
  • Coq
  • Mechanized proofs
  • Running-time

ASJC Scopus subject areas

  • Software

Fingerprint

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

Cite this