A Practical Mode System for Recursive Definitions
summary
A static mode system that classifies recursive bindings as safe or vicious and is proven sound against the Nordlander–Carlsson–Gill source semantics. It gives two complementary modes (roughly return vs construct) and a directed backwards algorithm extracted from declarative rules, replaces the fragile syntactic OCaml check, and is implemented in OCaml where it catches previously missed buggy definitions. Paper-level artifacts: declarative rules, a mechanistic soundness proof, and an executable OCaml implementation that scales to real-language features (exceptions, GADTs, first-class modules).
AI-written summary · about