Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Playing with the Tower of Hanoi Formally

Laurent Théry 1
1 STAMP - Sûreté du logiciel et Preuves Mathématiques Formalisées
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : 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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [8 references]  Display  Hide  Download

https://hal.inria.fr/hal-02903548
Contributor : Laurent Thery <>
Submitted on : Tuesday, July 21, 2020 - 11:53:48 AM
Last modification on : Wednesday, July 22, 2020 - 3:43:49 AM

File

Note.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02903548, version 2

Collections

Citation

Laurent Théry. Playing with the Tower of Hanoi Formally. 2020. ⟨hal-02903548⟩

Share

Metrics

Record views

109

Files downloads

876