Shoggoth - A Formal Foundation for Strategic Rewriting

Explore a formal foundation for strategic rewriting in this 18-minute conference talk from POPL'24. Delve into Shoggoth, a framework designed to understand, analyze, and reason about complex rewrite strategies. Learn how Shoggoth addresses semantic complexities such as nondeterminism, error-triggered backtracking, and potential non-termination. Discover the denotational semantics of System S, a core language for strategic rewriting, and its proven equivalence to an extended big-step operational semantics. Examine the location-based weakest precondition calculus introduced for formal reasoning about rewriting strategies, and understand its practical applications in proving termination, well-composition, and desired postconditions. Gain insights into the mechanized proofs and formalization in Isabelle/HOL, providing a robust foundation for strategic rewriting across various domains.