Object Calculus with First-Class Continuations

S.-y. Nishizaki and R. Ikeda (Japan)


Objectoriented programming language, firstclass contin uation, object calculus, operational semantics


Object calculus is a computational system proposed by Abadi and Cardelli that formalizes object-oriented features, such as lazy binding of self parameters, with simple syn tax and semantics. Continuations are computational states in execution systems, which represent pauses in computa tion. The mechanism of first-class continuation enables us to treat continuations as first-class entities; we can save the current continuation as data, or conversely, we can use the saved data as the current continuation. We implemented advanced control features in the mechanism including co routines and backtracks. In this paper, we introduce the first-class continuation into object calculus and propose continuation object calculus. Semantics in this new calcu lus are given as a weak reduction using evaluation contexts; first-class continuations are formalized as continuation ob jects with evaluation contexts in their fields. First, we pro pose untyped continuation object calculus. Then, we pro vide a first-order-type system to the calculus and show its subject reduction theorem. Finally, we introduce subtyping of the calculus and show its fundamental properties, such as the subject reduction theorem.

Important Links:

Go Back