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.
Type de document :
Article dans une revue
Higher-Order and Symbolic Computation, Springer Verlag, 2013
Liste complète des métadonnées


https://hal.inria.fr/inria-00629473
Contributeur : Yann Regis-Gianas <>
Soumis le : mercredi 16 janvier 2013 - 14:32:12
Dernière modification le : mercredi 12 octobre 2016 - 01:23:54
Document(s) archivé(s) le : mercredi 17 avril 2013 - 03:51:08

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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

Collections

INRIA | PPS | USPC

Citation

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

Partager

Métriques

Consultations de
la notice

357

Téléchargements du document

200