[PRL] Semi-automatic complexity analysis of a higher-order language. (arXiv:1206.3...

[Mitch]

fwiw..

Sent to you by Mitch via Google Reader: Semi-automatic complexity
analysis of a higher-order language. (arXiv:1206.3523v1 [cs.PL]) via
cs.PL updates on arXiv.org by <a
href="http://arxiv.org/find/cs/1/au:+Danner_N/0/1/0/all/0/1">N.
Danner</a>, <a
href="http://arxiv.org/find/cs/1/au:+Paykin_J/0/1/0/all/0/1">J.
Paykin</a>, <a
href="http://arxiv.org/find/cs/1/au:+Royer_J/0/1/0/all/0/1">J. S.
Royer</a> on 6/17/12

We develop a static cost analysis for a higher-order functional
language with structural list recursion. The cost of evaluating an
expression is defined to be the size of its big-step evaluation
derivation. The complexity of an expression is a pair consisting of a
cost and a potential, which is a measure of the "future" cost of using
the value of that expression. A translation function tr 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 tr(t) is an upper bound on the cost of evaluating t. The proof of
the Soundness Theorem is formalized in Coq, leading to certified upper
bounds on the cost of any expression in the target language.

Things you can do from here:
- Subscribe to cs.PL updates on arXiv.org using Google Reader
- Get started using Google Reader to easily keep up with all your
favorite sites
-------------- next part --------------
HTML attachment scrubbed and removed