2 papers
cs.LO2025
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…
cs.LO2024
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…