Termination in Higher-Order Concurrent Calculi

10 years 8 months ago
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 ...
Romain Demangeon, Daniel Hirschkoff, Davide Sangio
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where FSEN
Authors Romain Demangeon, Daniel Hirschkoff, Davide Sangiorgi
Comments (0)