Certifying and reasoning about cost annotations of functional programs
Programming Languages
2013-01-17 v2
Abstract
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 including safe memory management, and to reason on them in a higher-order Hoare logic.
Cite
@article{arxiv.1110.2350,
title = {Certifying and reasoning about cost annotations of functional programs},
author = {Roberto M. Amadio and Yann Regis-Gianas},
journal= {arXiv preprint arXiv:1110.2350},
year = {2013}
}
Comments
Higher-Order and Symbolic Computation (2013)