A Domain-theoretic Model for a Higher-order Process Calculus

In this paper we study a higher-order process calculus, a restriction of one due to Boudol, and develop an abstract, model for it. By abstract we mean that the model is constructed domain-theoretically and reflects a certain conceptual viewpoint about observability. It is not constructed from the syntax of the calculus or from computation sequences. We describe a new powerdomain construction that can be given additional algebraic structure that allows one to model concurrent composition, in the same sense that Plotkin's powerdomain can have a continuous binary operation defined on it to model choice. We show that the model constructed this way is adequate with respect to the operational semantics. The model that we develop and our analysis of it is closely related to the work of Abramsky and Ong on the lazy lambda calculus. 1 Introduction A fundamental problem in the semantics of parallel programming languages is integrating concurrency with abstraction. Kahn's pioneering work on stat..