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

Displayed time zone: Tijuana, Baja California change

15:45 - 16:45
Coinduction and TestingDeepSpec at 106B
Chair(s): Lennart Beringer Princeton University
15:45
30m
Talk
Coinductive Reasoning about Interaction Trees
DeepSpec
Chung-Kil Hur Seoul National University
16:15
30m
Talk
Coverage Guided, Property Based Testing
DeepSpec
Leonidas Lampropoulos University of Pennsylvania