Name
Abstract | ||
|---|---|---|
We introduce a type system for the π-calculus which is designed to guarantee that typable processes are well-behaved, namely they never produce a run-time error and, even if they may diverge, there is always a chance for them to “finish their work”, i.e., to reduce to an idle process. The introduced type system is based on non-idempotent intersections, and is thus very powerful as for the class of processes it can capture. Indeed, despite the fact that the underlying property is Π20-complete, there is a way to show that the system is complete, i.e., that any well-behaved process is typable, although for obvious reasons infinitely many derivations need to be considered.
|
Year | DOI | Venue |
|---|---|---|
2019 | 10.1145/3290320 | Proceedings of the ACM on Programming Languages |
Keywords | Field | DocType |
$\pi$-calculus,intersection types,linear logic,runtime error analysis | Computer science,Idle,Pi calculus,Theoretical computer science,Linear logic | Journal |
Volume | Issue | ISSN |
3 | POPL | 2475-1421 |
Citations | PageRank | References |
0 | 0.34 | 13 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ugo Dal Lago | 1 | 565 | 60.42 |
| Marc de Visme | 2 | 0 | 0.34 |
| Damiano Mazza | 3 | 58 | 9.27 |
| Akira Yoshimizu | 4 | 18 | 4.15 |