Object-Oriented Programming Language with Control Operators
Delimited continuations are being introduced into a wide range of programming languages. To ensure safety of languages with continuations, it is important to formalize those languages in a mathematical way, but most existing formalizations are developed for functional languages.
We formalize an object-oriented programming language that has delimited continuations. Our formalization is an extension of Featherweight Java with the delimited control operators shift and reset.