Resource Usage Analysis for the Pi-Calculus
<|reference_start|>Resource Usage Analysis for the Pi-Calculus: We propose a type-based resource usage analysis for the &#960;-calculus extended with resource creation/access primitives. The goal of the resource usage analysis is to statically check that a program accesses resources such as files and memory in a valid manner. Our type system is an extension of previous behavioral type systems for the &#960;-calculus, and can guarantee the safety property that no invalid access is performed, as well as the property that necessary accesses (such as the close operation for a file) are eventually performed unless the program diverges. A sound type inference algorithm for the type system is also developed to free the programmer from the burden of writing complex type annotations. Based on the algorithm, we have implemented a prototype resource usage analyzer for the &#960;-calculus. To the authors' knowledge, ours is the first type-based resource usage analysis that deals with an expressive concurrent language like the pi-calculus.<|reference_end|>
@article{kobayashi2006resource,
    title={Resource Usage Analysis for the Pi-Calculus},
    author={Naoki Kobayashi, Kohei Suenaga, and Lucian Wischik},
    journal={Logical Methods in Computer Science, Volume 2, Issue 3 (September
  13, 2006) lmcs:2246},
    year={2006},
    doi={10.2168/LMCS-2(3:4)2006},
    archivePrefix={arXiv},
    eprint={cs/0608035},
    primaryClass={cs.PL cs.LO}
}