UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Moessner's theorem: An exercise in coinductive reasoning in COQ

Krebbers, R; Parlant, L; Silva, A; (2016) Moessner's theorem: An exercise in coinductive reasoning in COQ. In: Abraham, E and Bonsangue, M and Johnsen, EB, (eds.) Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday. (pp. pp. 309-324). Springer International Publishing Green open access

[thumbnail of moessner.pdf]
Preview
Text
moessner.pdf - Accepted Version

Download (326kB) | Preview

Abstract

Moessner's Theorem describes a construction of the sequence of powers (1n, 2n, 3n,…), by repeatedly dropping and summing elements from the sequence of positive natural numbers. The theorem was presented by Moessner in 1951 without a proof and later proved and generalized in several directions. More recently, a coinductive proof of the original theorem was given by Niqui and Rutten. We present a formalization of their proof in the Coq proof assistant. This formalization serves as a non-trivial illustration of the use of coinduction in Coq. During the formalization, we discovered that Long and Salié's generalizations could also be proved using (almost) the same bisimulation.

Type: Proceedings paper
Title: Moessner's theorem: An exercise in coinductive reasoning in COQ
ISBN-13: 9783319307336
Open access status: An open access version is available from UCL Discovery
DOI: 10.1007/978-3-319-30734-3_21
Publisher version: http://dx.doi.org/10.1007/978-3-319-30734-3_21
Additional information: Copyright © 2016 Springer International Publishing Switzerland. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-30734-3_21
UCL classification: UCL
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/1492921
Downloads since deposit
Loading...
438Downloads
Download activity - last month
Loading...
Download activity - last 12 months
Loading...
Downloads by country - last 12 months
Loading...

Archive Staff Only

View Item View Item