Shall we juggle, coinductively?

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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
Pages160-172
Number of pages13
DOIs
Publication statusPublished - 2012
Externally publishedYes
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

Other

Other2nd International Conference on Certified Programs and Proofs, CPP 2012
CountryJapan
CityKyoto
Period12/12/1312/12/15

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

Cite this