Copenhagen Programming Language Seminar
In this talk I will give an overview of a recent work on the expressiveness of higher-order calculi. In higher-order process calculi the values exchanged in communications may contain processes. I will introduce HOcore, a core calculus of higher-order concurrency; it has only the operators necessary to express higher-order communications: input pre?x, process output, and parallel composition. By exhibiting a nearly deterministic encoding of Minsky Machines, HOcore is shown to be Turing Complete and therefore its termination problem is undecidable. Strong bisimilarity, however, is proved to be decidable. Further, the main forms of strong bisimilarity for higher-order processes (higher-order bisimilarity, context bisimilarity, normal bisimilarity, barbed congruence) coincide. They also coincide with their asynchronous versions. If time permits, I will discuss two additional results: (i) a sound and complete axiomatization of bisimilarity, and (ii) the proof that bisimilarity becomes undecidable if at least four static (i.e., top-level) restrictions are added to the calculus.
All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to email@example.com with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org