The draft will be updated a few times to improve the presentation of the final version. When I update it, I will include a summary of the changes that went into the new version.
Final version! Complete rewrite of the related work, threaded a small example in Chapter 4 to ease the presentation, and included many suggestions from Tom Reps (Thanks!).
Invariant logics of Chapter 2: InvariantLogic.v
Translation proofs for the stack quantitative logic of Chapter 3: LogicMorphisms1.v
Quantitative CompCert of Chapter 3: veristack.zip Also contains the implementation of the quantitative logic given to the AEC of PLDI'14.
Translation proof for tick quantitative logic of Chapter 4: LogicMorphisms2.v
Coq support library for the bound certificates of Chapter 6: pastis-coq.zip