From Enhanced Coinduction towards Enhanced Induction
summary
Claims a reusable theory that lifts bisimulation-style semiprogressions to inductive behavioral preorders by introducing inductive observables with numeric depths and a class of weight-preserving functions on relations. Uses model‑logic observables, local progression checks and induction-heavy soundness proofs to show R → F(R) implies R ⊆ the preorder, exhibits nontrivial examples (CCS‑like language), proves closure under composition and derives congruence and recursion preservation results, covering both strong and weak semantics.
AI-written summary · about
chapters (5)
- 0:00Start
- 9:49What Is an Inductive Reorder
- 12:23The Definition of the First Inductive Enhancement
- 18:32The Difference between Strong and Weak Semantics
- 22:20Why Do I Use Progression Semi Progressions
related talks
16mInductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline...
22mLayers of Confluence for Actors
28mReasoning about Distributed Reconfigurable Systems
25mSemantic Analysis of Normalisation for Directional Logic Programming
45mCorrectness proofs of distributed systems with Isabelle
21mA Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verifie...
25mStep-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Ch...
14mA Refinement Methodology for Distributed Programs in Rust