Playing with the Tower of Hanoi Formally
Résumé
The Tower of Hanoi is a typical example that illustrates all the power of recursion in programming. In this paper, we show that it is also a very nice example for inductive proofs and formal verification. We present some non-trivial results about it that have been formalised in the Coq proof assistant.
Domaines
Logique en informatique [cs.LO]
Origine : Fichiers produits par l'(les) auteur(s)
Loading...