Published June 29, 2021 | Version v1
Conference paper

Proof Pearl : Playing with the Tower of Hanoi Formally

Description

The Tower of Hanoi is a typical example that is used in computer science courses to illustrate all the power of recursion. 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 that have been formalised in the {Coq} proof assistant.

Abstract

International audience

Additional details

Identifiers

URL
https://hal.inria.fr/hal-03324274
URN
urn:oai:HAL:hal-03324274v1