This page complements a submission to TOPLAS; last update on 2013-09-20.


The development available here slightly differs from what is described in the paper. In particular the rely-guarantee methodology is encoded in a permission system.

Download the Coq development

[.tgz] (150kio, tested with Coq 8.3pl2 and CompCert-TSO 1.12)

Browse the Coq development

The syntax/semantic of the INJECT language

The syntax/semantic of the RTLinject language

The definition of refines and the compositional rules

Injected Code

Certified backend RTLinject → Asm

MIR compiler and sample programs