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

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

Research output: Contribution to journal › Article (Academic Journal)

13 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 2020 → 25 Jan 2020
Conference number: 2020
https://popl20.sigplan.org/

Bibliographical note

Provisional acceptance date added, based on publication information.

Structured keywords

  • Programming Languages

Keywords

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

Access to Document

  • Full-text PDF (final published version)

    This is the final published version of the article (version of record). It first appeared online via Association for Computing Machinery at https://dl.acm.org/doi/10.1145/3371083. Please refer to any applicable terms of use of the publisher.

    Final published version, 478 KBLicence: CC BY

    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