131 citations · 150 across the 7 of their papers we have counts for
8 papers
Coco: Corecursion with Compositional Heterogeneous Productivity
Jaewoo Kim, Yeonwoo Nam, Chung-Kil Hur
Contemporary proof assistants impose restrictive syntactic guardedness conditions that reject many valid corecursive definitions. Existing approaches to overcome these restrictions…
Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL
Simon Foster, Chung-Kil Hur, Jim Woodcock
Model execution allows us to prototype and analyse software engineering models by stepping through their possible behaviours, using techniques like animation and simulation. On the…
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…
Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL
Simon Foster, Chung-Kil Hur, Jim Woodcock
Simulation and formal verification are important complementary techniques necessary in high assurance model-based systems development. In order to support coherent results, it is n…
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…
On the mathematical synthesis of equational logics
Marcelo Fiore, Chung-Kil Hur
We provide a mathematical theory and methodology for synthesising equational logics from algebraic metatheories. We illustrate our methodology by means of two applications: a ratio…