Comment by xamuel

Here is the paper: http://arxiv.org/abs/1105.4135 And here is the formalization of sections 2-3 in Coq: http://www.math.osu.edu/~alexander.421/mech.txt