HP Labs Technical Reports
Click here for full text:
A Higher Order Logic Mechanization of the CSP FailureDivergence Semantics
Camilleri, Albert
HPL90194
Keyword(s):
Abstract: Reasoning using process algebras often involves doing complex proofs; computerbased support to facilitate the task is therefore desirable. In this paper we show how a generalpurpose 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 highlevel algebraic laws from the defitions as theorems. We mechanize a vari ation on the failuredivergence 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.
27 Pages
Back to Index
