[isabelle] Current CSP formalisation with syntax and semantics
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Current CSP formalisation with syntax and semantics
- From: JÃhnig, Nils Erik <nils.jaehnig at tu-berlin.de>
- Date: Tue, 3 May 2016 08:50:15 +0000
- Accept-language: en-US, de-DE
- Thread-index: AQHRpRjPkyPySeySYkyGRVRnPvS7Yw==
- Thread-topic: Current CSP formalisation with syntax and semantics
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and