Shall we juggle, coinductively?

Keisuke Nakano

doi:10.1007/978-3-642-35308-6_14

Shall we juggle, coinductively?

Keisuke Nakano

RIEC - Computing System Platforms Division

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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 language	English
Title of host publication	Certified Programs and Proofs - Second International Conference, CPP 2012, Proceedings
Pages	160-172
Number of pages	13
DOIs	https://doi.org/10.1007/978-3-642-35308-6_14
Publication status	Published - 2012
Event	2nd International Conference on Certified Programs and Proofs, CPP 2012 - Kyoto, Japan Duration: 2012 Dec 13 → 2012 Dec 15

Publication series

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

Conference

Conference	2nd International Conference on Certified Programs and Proofs, CPP 2012
Country/Territory	Japan
City	Kyoto
Period	12/12/13 → 12/12/15

Access to Document

10.1007/978-3-642-35308-6_14

Cite this

@inproceedings{cc901fb7c11c4b54b234495bd72326b5,

title = "Shall we juggle, coinductively?",

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.",

author = "Keisuke Nakano",

year = "2012",

doi = "10.1007/978-3-642-35308-6_14",

language = "English",

isbn = "9783642353079",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "160--172",

booktitle = "Certified Programs and Proofs - Second International Conference, CPP 2012, Proceedings",

note = "2nd International Conference on Certified Programs and Proofs, CPP 2012 ; Conference date: 13-12-2012 Through 15-12-2012",

}

Nakano, K 2012, Shall we juggle, coinductively? in Certified Programs and Proofs - Second International Conference, CPP 2012, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7679 LNCS, pp. 160-172, 2nd International Conference on Certified Programs and Proofs, CPP 2012, Kyoto, Japan, 12/12/13. https://doi.org/10.1007/978-3-642-35308-6_14

Shall we juggle, coinductively? / Nakano, Keisuke.
Certified Programs and Proofs - Second International Conference, CPP 2012, Proceedings. 2012. p. 160-172 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7679 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review