Type systems for concurrent programs. (English) Zbl 1274.68076
Aichernig, Bernhard K. (ed.) et al., Formal methods at the crossroads. From Panacea to foundational support. 10th anniversary colloquium of UNU/IIST, the International Institute for Software Technology of The United Nations University, Lisbon, Portugal, March 18–20, 2002. Revised papers. Berlin: Springer (ISBN 3-540-20527-6/pbk). Lect. Notes Comput. Sci. 2757, 439-453 (2003).
Summary: Type systems for programming languages help reasoning about program behavior and early finding of bugs. Recent applications of type systems include analysis of various program behaviors such as side effects, resource usage, security properties, and concurrency. This paper is a tutorial of one of such applications: type systems for analyzing behavior of concurrent processes. We start with a simple type system and extend it step by step to obtain more expressive type systems to reason about deadlock-freedom, safe usage of locks, etc.
For the entire collection see [Zbl 1028.00041].
For the entire collection see [Zbl 1028.00041].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
