Shin-ya Nishizaki and Ritsuya Ikeda
Object-oriented programming language, first-class continuation,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 syntax and semantics. Continuations are computational states in execution systems, which represent pauses in computation. 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 calculus are given as a weak reduction using evaluation contexts; first-class continuations are formalized as continuation objects with evaluation contexts in their fields. First, we propose untyped continuation object calculus. Then, we provide 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
