A Proof Pearl with the Fan Theorem and Bar Induction - Walking through Infinite Trees with Mixed Induction and Coinduction.

Keiko Nakata, Tarmo Uustalu, Marc Bezem

Browse the full APLAS paper archive.