[isabelle] Current CSP formalisation with syntax and semantics



Dear list,


I am looking for a CSP formalisation, where syntax and semantics are defined. Ideally, this formalisation works in Isabelle 2016.

Theories which aim for general properties of CSP only define the semantics of CSP, such as the theories by Pasquale Noce.

There is the CSP-Prover, by Yoshinao Isobe and Markus Roggenbach, which is not in the AFP. It defines both syntax and semantics of CSP, but does not work in Isabelle 2016.

Did I overlook something? Or do I have to make CSP-Prover work in Isabelle 2016 myself?


Best
Nils



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.