Blogmarks.net is a social bookmarking service.

Founded in late 2003 and heartquartered in France, we are non-profit and independant.

We believe in the open web, think internet services should be sustainable, build for the long term.

While we are re-launching the service, we only accept new members through invitation.

PUBLIC MARKS with tags del.icio.us & Coq

20 January 2006

The Compcert certified compiler back-end

by GeorgesMariano

The Compcert back-end is a compiler that generates PowerPC assembly code from a low-level intermediate language called Cminor and a slightly more expressive intermediate language called Csharpminor. The particularity of this compiler is that it is written

del.icio.us compiler OCaml formal-methods Coq

17 January 2006

Why: a software verification tool

by GeorgesMariano

Why aims at being a verification conditions generator (VCG) back-end for other verification tools. It provides a powerful input language including higher-order functions, polymorphism, references, arrays and exceptions. It generates proof obligations for

del.icio.us software tool why OCaml verification Coq prover