A static cost analysis for a higher-order language

Norman Danner, Jennifer Paykin, James S. Royer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

17 Scopus citations

Abstract

We develop a static complexity analysis for a higher-order functional language with structural list recursion. The complexity of an expression is a pair consisting of a cost and a potential. The former is defined to be the size of the expression's evaluation derivation in a standard big-step operational semantics. The latter is a measure of the "future" cost of using the value of that expression. A translation function maps target expressions to complexities. Our main result is the following Soundness Theorem: If t is a term in the target language, then the cost component of ktk is an upper bound on the cost of evaluating t. The proof of the Soundness Theorem is formalized in Coq, providing certified upper bounds on the cost of any expression in the target language.

Original languageEnglish (US)
Title of host publicationPLPV 2013 - Proceedings of the 2013 ACM SIGPLAN Workshop on Programming Languages Meets Program Verification, Co-located with POPL 2013
Pages25-34
Number of pages10
DOIs
StatePublished - 2013
Event2013 7th ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2013 - Co-located with POPL 2013 - Rome, Italy
Duration: Jan 22 2013Jan 22 2013

Publication series

NamePLPV 2013 - Proceedings of the 2013 ACM SIGPLAN Workshop on Programming Languages Meets Program Verification, Co-located with POPL 2013

Other

Other2013 7th ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2013 - Co-located with POPL 2013
CountryItaly
CityRome
Period1/22/131/22/13

Keywords

  • Automated theorem proving
  • Certified bounds
  • Higher-order complexity

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'A static cost analysis for a higher-order language'. Together they form a unique fingerprint.

  • Cite this

    Danner, N., Paykin, J., & Royer, J. S. (2013). A static cost analysis for a higher-order language. In PLPV 2013 - Proceedings of the 2013 ACM SIGPLAN Workshop on Programming Languages Meets Program Verification, Co-located with POPL 2013 (pp. 25-34). (PLPV 2013 - Proceedings of the 2013 ACM SIGPLAN Workshop on Programming Languages Meets Program Verification, Co-located with POPL 2013). https://doi.org/10.1145/2428116.2428123