Termination in Higher-Order Concurrent Calculi

Abstract. We study termination of programs in concurrent higherorder languages. A higher-order concurrent calculus combines features of the λ-calculus and of the message-passing concurrent calculi. However, in contrast with the λ-calculus, a simply-typed discipline need not guarantee termination; and, in contrast with message-passing calculi such as the π-calculus, divergence 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 (and following the approach to termination in the π-calculus in [DS06]). 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 ...

• Type: Conference
• Year: 2009
• Where: FSEN
• Authors: Romain Demangeon, Daniel Hirschkoff, Davide Sangiorgi
• Keywords: FSEN 2009, Message-passing Calculi, Message-passing Concurrent Calculi, Simply-typed Discipline, Software Engineering