TY - GEN
T1 - A static cost analysis for a higher-order language
AU - Danner, Norman
AU - Paykin, Jennifer
AU - Royer, James S.
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
KW - Automated theorem proving
KW - Certified bounds
KW - Higher-order complexity
UR - http://www.scopus.com/inward/record.url?scp=84873419135&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84873419135&partnerID=8YFLogxK
U2 - 10.1145/2428116.2428123
DO - 10.1145/2428116.2428123
M3 - Conference contribution
AN - SCOPUS:84873419135
SN - 9781450318600
T3 - PLPV 2013 - Proceedings of the 2013 ACM SIGPLAN Workshop on Programming Languages Meets Program Verification, Co-located with POPL 2013
SP - 25
EP - 34
BT - PLPV 2013 - Proceedings of the 2013 ACM SIGPLAN Workshop on Programming Languages Meets Program Verification, Co-located with POPL 2013
T2 - 2013 7th ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2013 - Co-located with POPL 2013
Y2 - 22 January 2013 through 22 January 2013
ER -