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.
Titolo: | Termination in Higher-Order Concurrent Calculi |
Autore/i: | R. D.e.m.a.n.g.e.o.n. D. Hirschkoff; SANGIORGI, DAVIDE |
Autore/i Unibo: | |
Anno: | 2009 |
Titolo del libro: | Lecture Notes in Computer Science |
Pagina iniziale: | 81 |
Pagina finale: | 96 |
Abstract: | 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. |
Data prodotto definitivo in UGOV: | 1-feb-2010 |
Appare nelle tipologie: | 4.01 Contributo in Atti di convegno |