WCET 2019 publication
Documentation of the Coq formalization (as hyperlinked HTML)
Coq source of the formalization (with proofs)