Page sem2009/abstracts/schmitt

Expressivity in higher order calculi Alan Schmitt INRIA Grenoble

We have recently shown that a fragment of the higher order pi calculus, called HO Core, is Turing complete yet its contextual congruence is decidable. The absence of name restriction is crucial for this latter property, but prevents compositional encodings. Adding name restriction allows for additional results, such as the ability to encode the synchronous higher order pi calculus in the asynchronous one, but we will show that for a large class of encodings, it is impossible to encode a polyadic higher order pi calculus into a monadic one. We will finally conjecture the existence of a whole hierarchy of impossibility results when not only processes but also functions may be sent in messages.