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.
Type de document :
Communication dans un congrès
Ricardo Peña. Foundational and Practical Aspects of Resource Analysis, May 2011, Madrid, Spain. Springer, 7177, pp.72-88, 2012, Lecture Notes in Computer Science; Foundational and Practical Aspects of Resource Analysis
Liste complète des métadonnées

https://hal.inria.fr/inria-00629473
Contributeur : Yann Regis-Gianas <>
Soumis le : mardi 11 octobre 2011 - 10:23:44
Dernière modification le : vendredi 6 février 2015 - 12:22:18
Document(s) archivé(s) le : jeudi 12 janvier 2012 - 02:21:02

Fichiers

lncs-fun-cca.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. Ricardo Peña. Foundational and Practical Aspects of Resource Analysis, May 2011, Madrid, Spain. Springer, 7177, pp.72-88, 2012, Lecture Notes in Computer Science; Foundational and Practical Aspects of Resource Analysis. <inria-00629473v1>

Partager

Métriques

Consultations de
la notice

116

Téléchargements du document

300