Termination in Higher-Order Concurrent Calculi

We study termination of programs in concurrent higher-order languages. A higher-order concurrent calculus combines features of the $lambda$-calculus and of the message-passing concurrent calculi. However, in contrast with the $lambda$-calculus, a simply-typed discipline need not guarantee termination; and, in contrast with message-passing calculi such as the $pi$-calculus, termination can be obtained even without a recursion (or replication) construct. We first consider a higher-order calculus where only processes can be communicated. We propose a type system for termination that borrows ideas from termination in Rewriting Systems. We then show how this type system can be adapted to accommodate higher-order functions in messages. Finally, we address termination in a richer calculus, that includes localities and a passivation construct, as well as name-passing communication. We illustrate the expressiveness of the type systems on a few examples.