  CSP-Agda is a library, which formalises the process algebra CSP in the
interactive theorem prover Agda using coinductive data types. In CSP-Agda, CSP
processes are in monadic form, which sup- ports a modular development of
processes. In this paper, we implement two main models of CSP, trace and stable
failures semantics, in CSP-Agda, and define the corresponding refinement and
equal- ity relations. Because of the monadic setting, some adjustments need to
be made. As an example, we prove commutativity of the external choice operator
w.r.t. the trace semantics in CSP-Agda, and that refinement w.r.t. stable
failures semantics is a partial order. All proofs and definitions have been
type checked in Agda. Further proofs of algebraic laws will be available in the
CSP-Agda repository.
