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

19 Citations (Scopus)
108 Downloads (Pure)

Abstract

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
Volume4
Issue numberPOPL
DOIs
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
https://popl20.sigplan.org/

Bibliographical note

Provisional acceptance date added, based on publication information.

Research Groups and Themes

  • Programming Languages

Keywords

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

Fingerprint

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

Cite this