The purpose of this webpage is to provide the Coq formalization discussed in:

Documentation:

Formalization as of 2017/01/06