HP Labs Technical Reports
Click here for full text:
A Higher Order Logic Mechanization of the CSP Failure-Divergence Semantics
Abstract: Reasoning using process algebras often involves doing complex proofs; computer-based support to facilitate the task is therefore desirable. In this paper we show how a general-purpose theorem prover based on higher order logic provides a natural framework for mechanising the process algebra CSP. This is done by defining the semantics of the CSP operators in the logic and proving the high-level algebraic laws from the defitions as theorems. We mechanize a vari- ation on the failure-divergence semantics that does not use alphabets at the syntatic level, but embeds them in the semantics. Our approach abstracts further from the explicit use of alphabets by modelling them as type variables. The result is a mechanized theory for a polymorphic formalization of CSP.
Back to Index