Hydra Ludica (work in progress)

This project is a mechanization in Coq of the Hydra Games, as studied in by L. Kirby and J.Paris in in a famous paper .
The theorems contained in that paper enjoy the following characteristics:

Current state of the project

Please follow this link .
This is clearly a work in progress, and all kind of critic or contribution is welcome.
All the files herein are under licence Cecill-B .