Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Logic/Constraint Programming and Concurrency: The Hard-Won Lessons of the Fifth Generation Computer Project Read chapter Read first chapter

2016 | OriginalPaper | Chapter

A Coq Library for Internal Verification of Running-Times

Authors : Jay McCarthy, Burke Fetscher, Max New, Daniel Feltey, Robert Bruce Findler

Published in: Functional and Logic Programming

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Proof Relevant Corecursive Resolution
next chapter A Transformational Approach to Parametric Accumulated-Cost Static Profiling
Footnotes
1
The definition of ret, and all other monadic operations, are in the supplementary material and our public Github repo. The types are the most interesting part, however, so we focus on them.
 
2
This is the case if BigNums are represented as lists of bits.
 
Literature
Altenkirch, T., Chapman, J., Uustalu, T.: Monads need not be endofunctors. In: Proceedings of the Foundations of Software Science and Computation Structure (2010)
Braun, W., Rem, M.: A logarithmic Implementation of Flexible Arrays. Eindhoven University of Technology, MR83/4 (1983)
Charguéraud, A.: Characteristic Formulae for Mechanized Program Verification. Ph.D. dissertation, Université Paris Diderot (Paris 7) (2010)
Charguéraud, A., Pottier, F.: Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. In: Proceedings of the ITP (2015)
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. MIT Press, Cambridge (2009)MATH
Crary, K., Weirich, S.: Resource bound certification. In: Proceedings of the POPL (2000)
Crosby, S.A., Wallach, D.S.: Denial of service via algorithmic complexity attacks. In: Proceedings of the USENIX Security Symposium (2003)
Danielsson, N.A.: Lightweight semiformal time complexity analysis for purely functional data structures. In: Proceedings of the POPL (2008)
Danner, N., Paykin, J., Royer, J.S.: A static cost analysis for a higher-order language. In: Proceedings of the Workshop on Programming Languages meets Program Verification (2013)
Filliâtre, J.-C., Letouzey, P.: Functors for proofs and programs. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 370–384. Springer, Heidelberg (2004)CrossRef
Gulwani, S., Mehra, K.K., Chilimbi, T.: SPEED: precise and efficient static estimation of program computational complexity. In: Proceedings of the POPL (2009)
Hoffmann, J., Shao, Z.: Automatic static cost analysis for parallel programs. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 132–157. Springer, Heidelberg (2015)CrossRef
Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: Proceedings of the POPL (2003)
Hughes, J., Pareto, L.: Recursion and Dynamic Data-structures in bounded space: towards embedded ML programming. In: Proceedings of the ICFP (1999)
Rosendahl, M.: Automatic complexity analysis. In: Proceedings of the International Conference on Functional Programming Languages And Computer Architecture (1989)
Sozeau, M.: Subset coercions in Coq. In: Proceedings of the TYPES (2006)
Swamy, N., Weinberger, J., Schlesinger, C., Chen, J., Livshits, B.: Verifying higher-order programs with the dijkstra monad. In: Proceedings of the PLDI (2013)
Swierstra, W.: A hoare logic for the state monad. In: Proceedings of the TPHOLS (2009)
van der Weegen, E., McKinna, J.: A machine-checked proof of the average-case complexity of quicksort in Coq. In: Berardi, S., Damiani, F., de’Liguoro, U. (eds.) TYPES 2008. LNCS, vol. 5497, pp. 256–271. Springer, Heidelberg (2009)CrossRef
Xi, H.: Dependently typed data structures. In: Proceedings of the Workshop on Algorithmic Aspects of Advanced Programming Languages (1999a)
Xi, H.: Dependently Types in Practical Programming. Ph.D. dissertation, Carnegie Mellon University (1999b)
Xi, H., Pfenning, F.: Dependently types in practical programming. In: Proceedings of the POPL (1999)
Metadata
Title
A Coq Library for Internal Verification of Running-Times
Authors
Jay McCarthy
Burke Fetscher
Max New
Daniel Feltey
Robert Bruce Findler
Copyright Year
2016
Book
Functional and Logic Programming

Print ISBN: 978-3-319-29603-6

Electronic ISBN: 978-3-319-29604-3

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-319-29604-3_10

Premium Partner

    Image Credits