Quentin Carbonneaux
Ph.D. Dissertation

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.

Versions

• 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!).

Coq proofs

• 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