AbstractThe pi-calculus is a process algebra for modelling concurrent systems in which the pattern of communication between processes may change over time. This paper describes the results of preliminary work on a definitional formal theory of the pi-calculus in higher order logic using the HOL theorem prover. The ultimate goal of this work is to provide practical mechanized support for reasoning with the pi-calculus about applications.
Categories and Subject Descriptors: F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages; D.2.1 [Software Engineering]: Requirements/Specifications; D.2.4 [Software Engineering]: Program Verification
Selected references
- R J R Back and J von Wright. Refinement concepts formalised in higher order logic. Formal Aspects of Computing, 2(3):247-272, 1990.
- Albert John Camilleri. Mechanizing CSP trace theory in higher order logic. IEEE Transactions on Software Engineering, 16(9):993-1004, September 1990.
- Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137-161, January 1985.
- Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I. Information and Computation, 100(1):1-40, September 1992.
- Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, II. Information and Computation, 100(1):41-77, September 1992.