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

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

doi:10.1145/3371083

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) › peer-review

19 Citations (Scopus)

116 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 language	English
Article number	15
Number of pages	31
Journal	Proceedings of the ACM on Programming Languages
Volume	4
Issue number	POPL
DOIs	https://doi.org/10.1145/3371083
Publication status	Published - 20 Dec 2019
Event	47th 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.

Research Groups and Themes

Programming Languages

Keywords

semantics
cost analysis
resource analysis
lambda calculus
recursion

Access to Document

10.1145/3371083

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

https://arxiv.org/abs/1911.04588

Handle.net

Persistent link

Dr Alex Kavvos
- alex.kavvosbristol.acuk
- School of Computer Science - Senior Lecturer
Person: Academic

Cite this

@article{14867d08cef840c4a33c6a929f14f569,

title = "Recurrence extraction for functional programs through call-by-push-value",

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.",

keywords = "semantics, cost analysis, resource analysis, lambda calculus, recursion",

author = "Kavvos, \{G. A.\} and Edward Morehouse and Daniel Licata and Norman Danner",

note = "Provisional acceptance date added, based on publication information. ; 47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020), POPL ; Conference date: 19-01-2020 Through 25-01-2020",

year = "2019",

month = dec,

day = "20",

doi = "10.1145/3371083",

language = "English",

volume = "4",

journal = "Proceedings of the ACM on Programming Languages",

issn = "2475-1421",

publisher = "Association for Computing Machinery",

number = "POPL",

url = "https://popl20.sigplan.org/",

}

TY - JOUR

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

AU - Kavvos, G. A.

AU - Morehouse, Edward

AU - Licata, Daniel

AU - Danner, Norman

N1 - Conference code: 2020

PY - 2019/12/20

Y1 - 2019/12/20

N2 - 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.

AB - 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.

KW - semantics

KW - cost analysis

KW - resource analysis

KW - lambda calculus

KW - recursion

U2 - 10.1145/3371083

DO - 10.1145/3371083

M3 - Article (Academic Journal)

SN - 2475-1421

VL - 4

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - POPL

M1 - 15

T2 - 47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020)

Y2 - 19 January 2020 through 25 January 2020

ER -

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

Abstract

Bibliographical note

Research Groups and Themes

Keywords

Access to Document

Handle.net

Fingerprint

Profiles

Dr Alex Kavvos

Cite this