Skip to Main content Skip to Navigation
New interface
Journal articles

Certifying and reasoning about cost annotations of functional programs

Roberto M. Amadio 1 Yann Régis-Gianas 1, 2 
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
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.
Document type :
Journal articles
Complete list of metadata

Cited literature [29 references]  Display  Hide  Download
Contributor : Yann Regis-Gianas Connect in order to contact the contributor
Submitted on : Wednesday, January 16, 2013 - 2:32:12 PM
Last modification on : Friday, January 21, 2022 - 3:22:15 AM
Long-term archiving on: : Wednesday, April 17, 2013 - 3:51:08 AM


Files produced by the author(s)


  • HAL Id : inria-00629473, version 2
  • ARXIV : 1110.2350



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



Record views


Files downloads