### Formalising Process Calculi in Higher Order Logic

### Abstract

In the past few years, several methods and tools based on
* process calculi * have been developed for verifying
properties of concurrent and communicating systems.
In this dissertation the interactive theorem prover HOL is used as a
framework for supporting reasoning about process calculi based on all the
various components of their formal theory. The aim is to build
a sound and effective tool to allow both verification of process
specifications and meta-theoretic reasoning.
In particular, the process calculus CCS is embedded in the
HOL logic. This is achieved by first addressing the pure subset of this
calculus (no value passing) and then extending it to its value-passing
version.
The CCS theory is mechanised in HOL by following a * purely
definitional* approach. This means that new objects are
embedded in HOL using definition mechanisms which guarantee that no
inconsistencies are introduced in the logic, and by deriving new facts from
definitions and/or previously proved theorems by formal proof.
Pure CCS agent expressions are encoded as a type in the HOL logic,
in which initially actions are represented as strings, agents with infinite
behaviour are given through the *rec*-notation and
agent summation is the usual binary operator.
Recursive agents are then allowed to be defined through systems of recursive
equations and to be parameterised. This makes the type of CCS expressions
polymorphic and parameterised on the parameters' type.
Operational and behavioural semantics and a modal logic
are defined and their properties and laws derived in HOL.
Several proof tools, such as inference rules, conversions and tactics, are
developed to enable users to carry out their proofs in an interactive way
and to automate them whenever possible.
Properties of infinite state systems, e.g. a counter which can expand
indefinitely, can be formally verified in the resulting proof environment.

Then, value-passing CCS is mechanised in HOL by translating value-passing
expressions into pure ones. This entails a more general polymorphic type
for pure agent expressions that includes an indexed summation operator.
The translation is proved to be *correct* with respect to the semantics
of value-passing CCS and then used at *meta-level*, together with
the HOL formalisation for pure CCS, for developing
behavioural theories for the value-passing calculus.
A proof environment is thus derived, in which users will directly work on
value-passing specifications. A verification example illustrates how
proofs about the data are neatly separated from proofs
about the process behaviour and how *omega-data-rules*
can be used in a practical way to reason
about value-passing agents defined over an infinite value domain.