PLDI 2019 (series) / DeepSpec 2019 (series) / DeepSpec 2019 /
Coinductive Reasoning about Interaction Trees
Interaction trees (ITrees) give a general-purpose data structure in Coq for formalizing the behaviors of recursive programs that interact with their environment. In order to permit infinite behaviors, ITrees are naturally defined as coinductive trees thereby requiring coinductive reasoning. In this talk, I will present an interesting coinductive proof structure for reasoning about equivalence up to taus (i.e., silent steps) between ITrees. The proofs can simultaneously carry two coinductive structures: weaker coinduction hypotheses guarded by any (silent or visible) steps, and stronger ones guarded by only visible steps. Interestingly, the weaker hypotheses do not survive under rewrites up to silent steps, while the stronger ones do. I will also talk about how to mechanize the proof structure in Coq using the Paco library, which provides general coinduction principles and Coq tactics.
Sun 23 Jun
|15:45 - 16:15|
Chung-Kil HurSeoul National University
|16:15 - 16:45|
Leonidas LampropoulosUniversity of Pennsylvania