From Mike Stay's PhD we posit modelling stability in a complex distributed system. Requires a transformation such a Laplace that deals with “stuff happening”. I was looking at applicative bisimulation. i.e. higher level type systems in the π-calculus page 
> "My recent Cambridge PhD thesis may be of interest. In it I define a small functional language and on it a typed form of applicative bisimulation. I use Howe's method from LICS'89 to show that applicative bisimulation is a congruence, and then prove the validity of a collection of equational properties of applicative bisimulation. These equational properties could be used to justify program transformations used in a compiler, say."
Greg (@leithaus) Meredith re-pointed me.
> "Applicative bisimulation is appropriate to applicative models of computation such as the lambda calculus. It doesn’t make much sense for concurrent models like pi or rho calculus."
Leading us to: The λ-calculus in the π-calculus by Xiaojuan Cai and Yuxi F paper We prefer this link at Shanghai Jiaotong University pdf
> "A general approach is proposed that transforms, in the framework of pi calculus, objects to methods in an on-the-fly manner. The power of the approach is demonstrated by applying it to generate an encoding of the full lambda calculus in the pi calculus. The encoding is proved to preserve and reflect beta reduction and is shown to be fully
abstract with respect to Abramsky’s applicative bisimilarity"
Leaves us wondering did Mike Stay, Greg Meredith and Sophia Drossopoulou discover that a new type system is required to keep a higher order programming system that can handle "stuff happening" capabilities based? Policy as Types in Object-capabilities # IDK.