CRIS Current Research Information System
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishWe 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 |
File in questo prodotto:
Copyright © 2020