Preprint
Sep 2026
Typed Flexible-Arity Slotted E-Graphs: A Soundness Construction and an Alloy Case Study
A generic finite quotient presentation proves exactness of its least-orbit normal form, while certified records specify effective-support kernel extraction and collision and abstract obligation traces carrying local endpoint certificates prove finite-unfolding equational soundness.
Guan-Xuan Wu, Allison Sullivan
· 0 citations