Certifying and reasoning about cost annotations of functional programs - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Journal Articles Higher-Order and Symbolic Computation Year : 2013

Certifying and reasoning about cost annotations of functional programs

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.

Domains

Programming Languages [cs.PL]
Fichier principal
Vignette du fichier
main.pdf (466.52 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Yann Regis-Gianas  : Connect in order to contact the contributor

https://inria.hal.science/inria-00629473

Submitted on : Wednesday, January 16, 2013-2:32:12 PM

Last modification on : Friday, March 24, 2023-2:52:56 PM

Long-term archiving on: Wednesday, April 17, 2013-3:51:08 AM

Download

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⟩

Export

BibTeX XML-TEI Dublin Core DC Terms EndNote DataCite

Collections

UNIV-PARIS7 PPS CNRS INRIA INRIA2
398 View
397 Download

Altmetric

Share

Gmail Facebook X LinkedIn More