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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Dec 20, 2019
- Source ID
- 10.1145/3371083
Entities
People
- Daniel R. Licata
- Edward Morehouse
- G. A. Kavvos
- Norman Danner
Organizations
- Air Force Office of Scientific Research
- National Science Foundation
- Wesleyan University