Certifying and reasoning about cost annotations of functional programs - Archive ouverte HAL Access content directly
Journal Articles Higher-Order and Symbolic Computation Year : 2013

Certifying and reasoning about cost annotations of functional programs

(1) , (1, 2)
1
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 including safe memory management, and to reason on them in a higher-order Hoare logic.
Fichier principal
Vignette du fichier
main.pdf (466.52 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00629473 , version 1 (11-10-2011)
inria-00629473 , version 2 (16-01-2013)

Identifiers

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

Cite

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

Altmetric

Share

Gmail Facebook Twitter LinkedIn More