Shall we juggle, coinductively?

研究成果: Conference contribution

抄録

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.

本文言語English
ホスト出版物のタイトルCertified Programs and Proofs - Second International Conference, CPP 2012, Proceedings
ページ160-172
ページ数13
DOI
出版ステータスPublished - 2012
外部発表はい
イベント2nd International Conference on Certified Programs and Proofs, CPP 2012 - Kyoto, Japan
継続期間: 2012 12月 132012 12月 15

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
7679 LNCS
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

Other

Other2nd International Conference on Certified Programs and Proofs, CPP 2012
国/地域Japan
CityKyoto
Period12/12/1312/12/15

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「Shall we juggle, coinductively?」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル