Certifying and reasoning about cost annotations of functional programs

Roberto M. Amadio, Yann Regis-Gianas

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 t…