inria-00629473, version 2
Certifying and reasoning about cost annotations of functional programs
Roberto M. Amadio
1Yann Regis-Gianas a, 1, 2
Higher-Order and Symbolic Computation (2013)
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.
- a – Université Paris-Diderot - Paris VII
- 1: Preuves, Programmes et Systèmes (PPS)
- CNRS : UMR7126 – Université Paris VII - Paris Diderot
- 2: PI.R2 (INRIA Paris - Rocquencourt)
- INRIA – Université Paris VII - Paris Diderot – CNRS : UMR7126
- Domain : Computer Science/Programming Languages
- Available versions : v1 (2011-10-11) v2 (2013-01-16)
- inria-00629473, version 2
- http://hal.inria.fr/inria-00629473
- oai:hal.inria.fr:inria-00629473
- From: Yann Regis-Gianas
- Submitted on: Wednesday, 16 January 2013 14:32:12
- Updated on: Wednesday, 16 January 2013 14:40:53
Associated documents
Export