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 JunDisplayed time zone: Tijuana, Baja California change
Sun 23 Jun
Displayed time zone: Tijuana, Baja California change
15:45 - 16:45 | |||
15:45 30mTalk | Coinductive Reasoning about Interaction Trees DeepSpec Chung-Kil Hur Seoul National University | ||
16:15 30mTalk | Coverage Guided, Property Based Testing DeepSpec Leonidas Lampropoulos University of Pennsylvania |