Flattening Meets Effects: A Surprising Connection
summary
Claims a concrete link between algebraic-effects metal language and term-rewriting termination techniques, showing HORPO-style ordering can be extended to handle lambda, application and a let form by combining RPO with the top-top lifting normalization proof; proves strong normalization for a restricted class of effect rewrites and reproduces a shorter, machine-checkable argument that replaces a brittle 20-page proof; fails so far to handle rewrites that commute effects out of nested lets (the original NRC flattening case) and remains work in progress seeking collaborators.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:01Three converging research lines
- 2:49Compiler translation motivation
- 5:24Core rewrite rules
- 7:11Meta language for effects
- 10:21Rewrite systems as effects
- 11:23Meta language with effects
- 13:30Extending RPO to effects
- 14:11Rewriting and termination
- 19:31Higher-order RPO challenges
- 22:01Limitations and work in progress
- 24:10Future directions
- 25:37Q&A
related talks
14mAdequacy for Algebraic Effects Revisited
32mVerifying Haskell's Rewrite Rules based on Polymorphic Rewriting Theory
54mRevisiting the Evolution of Effects (Invited Talk)
23mAnswer Refinement Modification: Refinement Type System for Algebraic Effects and...
21mVerifying term graph optimizations using Isabelle/HOL
21mEffectful Software Contracts
15mLatent Effects for Reusable Language Components
25mA Relational Separation Logic for Effect Handlers