Purity of an ST monad: full abstraction by semantically typed back-translation
summary
Proves that embedding a pure call-by-value language into an extension with an ST monad is fully abstract: contextual equivalences from the pure language remain valid with ST. Key construction is a two-step back-translation that first maps impure contexts into a semantically typed back-translation (an intermediate language carrying semantic type invariants) and then uses a universal type encoding to produce syntactically well-typed pure contexts. Proof is mechanized in Coq + Iris.
AI-written summary · about