Flattening Meets Effects - A Surprising Connection

Explore a surprising connection between term-rewriting systems and algebraic effects in this 35-minute conference talk from ACM SIGPLAN's HOPE'23. Delve into Ezra e. k. Cooper's research, which bridges the gap between these two areas of computer science. Discover how the Higher-Order Recursive Path Ordering (HORPO) scheme, typically used for proving termination in rewrite systems, can be applied to algebraic-effect systems. Learn about the potential extension of HORPO to cover rewrites involving the "let" construct, a common feature in many programming languages. Gain insights into this innovative approach that may lead to new developments in both term-rewriting and algebraic effects.