Certifying and reasoning on cost annotations of functional programs

Roberto M. Amadio 1 Yann Regis-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, and to reason on them in a higher-order Hoare logic.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00629473
Contributor : Yann Regis-Gianas <>
Submitted on : Tuesday, October 11, 2011 - 10:23:44 AM
Last modification on : Friday, January 4, 2019 - 5:33:25 PM
Long-term archiving on : Thursday, January 12, 2012 - 2:21:02 AM

Files

lncs-fun-cca.pdf
Files produced by the author(s)

Identifiers

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

Collections

PPS

Citation

Roberto M. Amadio, Yann Regis-Gianas. Certifying and reasoning on cost annotations of functional programs. Foundational and Practical Aspects of Resource Analysis, May 2011, Madrid, Spain. pp.72-88. ⟨inria-00629473v1⟩

Share

Metrics

Record views

157

Files downloads

340