zbMATH — the first resource for mathematics

Certifying and reasoning on cost annotations of functional programs. (English) Zbl 1367.68046
Peña, Ricardo (ed.) et al., Foundational and practical aspects of resource analysis. Second international workshop, FOPARA 2011, Madrid, Spain, May 19, 2011. Revised selected papers. Berlin: Springer (ISBN 978-3-642-32494-9/pbk). Lecture Notes in Computer Science 7177, 72-89 (2012).
Summary: We present a so-called labelling method to insert cost annotations in a higher-order functional program, to certify their correctness with respect to a standard compilation chain to assembly code, and to reason on them in a higher-order Hoare logic.
For the entire collection see [Zbl 1250.68046].

68N18 Functional programming and lambda calculus
03B70 Logic in computer science
Full Text: DOI