131 citations · 150 across the 7 of their papers we have counts for
4 papers · 1 filter
Conditional Contextual Refinement (CCR)
Youngju Song, Minki Cho, Dongjae Lee +1
Contextual refinement (CR) is one of the standard notions of specifying open programs. CR has two main advantages: (i) (horizontal and vertical) compositionality that allows us to…
Abstraction Logic: The Marriage of Contextual Refinement and Separation Logic
Youngju Song, Minki Cho, Dongjae Lee +1
Contextual refinement and separation logics are successful verification techniques that are very different in nature. First, the former guarantees behavioral refinement between a c…
An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
Yannick Zakowski, Paul He, Chung-Kil Hur +1
Coinductive reasoning about infinitary structures such as streams is widely applicable. However, practical frameworks for developing coinductive proofs and finding reasoning princi…
Interaction Trees: Representing Recursive and Impure Programs in Coq
Li-yao Xia, Yannick Zakowski, Paul He +4
"Interaction trees" (ITrees) are a general-purpose data structure for representing the behaviors of recursive programs that interact with their environments. A coinductive variant…