TY - GEN
T1 - A proof pearl with the fan theorem and bar induction
T2 - 9th Asian Symposium on Programming Languages and Systems, APLAS 2011
AU - Nakata, Keiko
AU - Uustalu, Tarmo
AU - Bezem, Marc
PY - 2011
Y1 - 2011
N2 - We study temporal properties over infinite binary red-blue trees in the setting of constructive type theory. We consider several familiar path-based properties, typical to linear-time and branching-time temporal logics like LTL and CTL *, and the corresponding tree-based properties, in the spirit of the modal μ-calculus. We conduct a systematic study of the relationships of the path-based and tree-based versions of "eventually always blueness" and mixed inductive-coinductive "almost always blueness" and arrive at a diagram relating these properties to each other in terms of implications that hold either unconditionally or under specific assumptions (Weak Continuity for Numbers, the Fan Theorem, Lesser Principle of Omniscience, Bar Induction). We have fully formalized our development with the Coq proof assistant.
AB - We study temporal properties over infinite binary red-blue trees in the setting of constructive type theory. We consider several familiar path-based properties, typical to linear-time and branching-time temporal logics like LTL and CTL *, and the corresponding tree-based properties, in the spirit of the modal μ-calculus. We conduct a systematic study of the relationships of the path-based and tree-based versions of "eventually always blueness" and mixed inductive-coinductive "almost always blueness" and arrive at a diagram relating these properties to each other in terms of implications that hold either unconditionally or under specific assumptions (Weak Continuity for Numbers, the Fan Theorem, Lesser Principle of Omniscience, Bar Induction). We have fully formalized our development with the Coq proof assistant.
UR - http://www.scopus.com/inward/record.url?scp=84055193127&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-25318-8_26
DO - 10.1007/978-3-642-25318-8_26
M3 - Conference contribution
AN - SCOPUS:84055193127
SN - 9783642253171
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 353
EP - 368
BT - Programming Languages and Systems - 9th Asian Symposium, APLAS 2011, Proceedings
Y2 - 5 December 2011 through 7 December 2011
ER -