Checking Equivalence in a Non-strict Language
summary
Nebula implements a fully automated co-induction calculus and symbolic executor for equivalence checking in non-strict Haskell, proving 22 of 24 valid generalized rewrite rules and finding concrete counterexamples for all 61 originally-invalid theorems from the Isabelle/Zeno suite; modified theorems with totality/ finiteness constraints verify 11/18 and 12/56 respectively. The tool synthesizes lemmas automatically and detects cycle counterexamples (32 found of 44 restricted cases), and supports symbolic function handling without concretization.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 2:08Lemma generation for co-induction
- 5:43Cycle counterexamples in symbolic execution
- 7:52Nebula performance
- 11:42Future directions
- 13:07Contributions and release
- 14:13Q&A
related talks
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
15mHEC: Equivalence Verification Checking for Code Transformation via Equality...
14mAdequacy for Algebraic Effects Revisited
19mAutomated Verification of Fundamental Algebraic Laws
28mFormalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
32mVerifying Haskell's Rewrite Rules based on Polymorphic Rewriting Theory
01h 06mVerifying a compiler through equational means
34mLiquid Haskell: Verification with Refinement Types