Certifying and reasoning about cost annotations of functional programs

Roberto M. Amadio (1) , Yann Régis-Gianas (1, 2)

1 PPS - Preuves, Programmes et Systèmes
2 PI.R2 - Design, study and implementation of languages for proofs and programs

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.

Domaines: Langage de programmation [cs.PL]

Roberto M. Amadio, Yann Régis-Gianas. Certifying and reasoning about cost annotations of functional programs. Higher-Order and Symbolic Computation, 2013. ⟨inria-00629473v2⟩