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:
- Most of their statements are easy to understand (the rules of hydra games and the termination of all games)
- The second part of their Theorem 2 is an opportunity of exploring
which tools are useful or necessary for proving that termination:
ordinals, canonical sequences of ordinals, rapidly growing functions, etc.
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 .