A generalization of exceptions and control in ML-like languages
Carl A. Gunter, Didier Rémy, Jon G. Riecke · 1995
We add functional continuations and prompts to a language with an ML-style type system.The operators significantly extend and simplify the control operators in SML/NJ, and can be themselves used to implement (simple) exceptions.We prove that well-typed terms never produce run-time type errors and give a module for implementing them in the latest version of SML/NJ.