Shall we juggle, coinductively?

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review


Buhler et al. presented a mathematical theory of toss juggling by regarding a toss pattern as an arithmetic function, where the function must satisfy a condition for the pattern to be valid. In this paper, the theory is formalized in terms of coinduction, reflecting the fact that the validity of toss juggling is related to a property of infinite phenomena. A tactic is implemented for proving the validity of toss patterns in Coq. Additionally, the completeness and soundness of a well-known algorithm for checking the validity is demonstrated. The result exposes a practical aspect of coinductive proofs.

Original languageEnglish
Title of host publicationCertified Programs and Proofs - Second International Conference, CPP 2012, Proceedings
Number of pages13
Publication statusPublished - 2012
Event2nd International Conference on Certified Programs and Proofs, CPP 2012 - Kyoto, Japan
Duration: 2012 Dec 132012 Dec 15

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7679 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference2nd International Conference on Certified Programs and Proofs, CPP 2012


Dive into the research topics of 'Shall we juggle, coinductively?'. Together they form a unique fingerprint.

Cite this