A formalization of the Grappa PPL in Coq - View it on GitHub