131 citations · 150 across the 7 of their papers we have counts for
4 papers · 1 filter
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…
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…
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…