Denotational Semantics for a Higher-Order Extension of the Monadic π-Calculus

We study a version of the higher-order #-calculus where transmittable items include items of ground type, such as communication channel names, but functions into processes as well. After providing operational semantics to the language we lay out a basic equational theory # which includes interleaving and normal form laws. We then construct a denotational model by solving an appropriate domain equation in a functor category. We provide explicit constructions of the syntactic operators and demonstrate (1) that the equational theory # presented is valid in the model. Finally, (2) we derive from validity of # a Computational Adequacy Theorem for the model