[PRL] Certifying and reasoning on cost annotations of functional programs. (arXiv:...

Mitch mwand1 at gmail.com
Fri Oct 14 10:59:03 EDT 2011


Possibly of interest to somebody here. (Evaluation based on abstract
only).

Sent to you by Mitch via Google Reader: Certifying and reasoning on
cost annotations of functional programs. (arXiv:1110.2350v1 [cs.PL])
via cs.PL updates on arXiv.org by <a
href="http://arxiv.org/find/cs/1/au:+Amadio_R/0/1/0/all/0/1">Roberto M.
Amadio</a> (PPS), <a
href="http://arxiv.org/find/cs/1/au:+Regis_Gianas_Y/0/1/0/all/0/1">Yann
Regis-Gianas</a> (PPS, INRIA Paris - Rocquencourt) on 10/11/11

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.

Things you can do from here:
- Subscribe to cs.PL updates on arXiv.org using Google Reader
- Get started using Google Reader to easily keep up with all your
favorite sites
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the PRL mailing list