Certifying and reasoning on cost annotations of functional programs
RM Amadio, Y Régis-Gianas - … on Foundational and Practical Aspects of …, 2011 - Springer
RM Amadio, Y Régis-Gianas
International Workshop on Foundational and Practical Aspects of Resource Analysis, 2011•SpringerLNCS 7177 - Certifying and Reasoning on Cost Annotations of Functional Programs Page 1
Certifying and Reasoning on Cost Annotations of Functional Programs Roberto M. Amadio1
and Yann Régis-Gianas1,2 1 Université Paris Diderot (UMR-CNRS 7126) 2 INRIA (Team πr
2 ) 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, and to reason on them in a higher-order Hoare logic. 1 Introduction In a …
Certifying and Reasoning on Cost Annotations of Functional Programs Roberto M. Amadio1
and Yann Régis-Gianas1,2 1 Université Paris Diderot (UMR-CNRS 7126) 2 INRIA (Team πr
2 ) 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, and to reason on them in a higher-order Hoare logic. 1 Introduction In a …
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, and to reason on them in a higher-order Hoare logic.
Springer
