Recurrence extraction for functional programs through call-by-push-value

G. A. Kavvos, Edward Morehouse, Daniel Licata, Norman Danner

Research output: Contribution to journalArticle (Academic Journal)peer-review

13 Citations (Scopus)
79 Downloads (Pure)


The main way of analysing the complexity of a program is that of extracting and solving a recurrence that expresses its running time in terms of the size of its input. We develop a method that automatically extracts such recurrences from the syntax of higher-order recursive functional programs. The resulting recurrences, which are programs in a call-by-name language with recursion, explicitly compute the running time in terms of the size of the input. In order to achieve this in a uniform way that covers both call-by-name and call-by-value evaluation strategies, we use Call-by-Push-Value (CBPV) as an intermediate language. Finally, we use domain theory to develop a denotational cost semantics for the resulting recurrences.
Original languageEnglish
Article number15
Number of pages31
JournalProceedings of the ACM on Programming Languages
Issue numberPOPL
Publication statusPublished - 20 Dec 2019
Event47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020) - JW Marriott New Orleans, New Orleans, United States
Duration: 19 Jan 202025 Jan 2020
Conference number: 2020

Bibliographical note

Provisional acceptance date added, based on publication information.

Structured keywords

  • Programming Languages


  • semantics
  • cost analysis
  • resource analysis
  • lambda calculus
  • recursion


Dive into the research topics of 'Recurrence extraction for functional programs through call-by-push-value'. Together they form a unique fingerprint.

Cite this