Sun 23 Jun 2019 15:45 - 16:15 at 106B - Coinduction and Testing Chair(s): Lennart Beringer
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
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

15:45 - 16:45: DeepSpec 2019 - Coinduction and Testing at 106B
Chair(s): Lennart BeringerPrinceton University
deepspec-2019-papers15:45 - 16:15
Chung-Kil HurSeoul National University
deepspec-2019-papers16:15 - 16:45
Leonidas LampropoulosUniversity of Pennsylvania