Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Current CSP formalisation with syntax and sema...

view this post on Zulip Email Gateway (Aug 22 2022 at 13:25):

From: "Jähnig, Nils Erik" <nils.jaehnig@tu-berlin.de>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 13:26):

From: Makarius <makarius@sketis.net>
The website https://staff.aist.go.jp/y-isobe/CSP-Prover/CSP-Prover.html
provides a version for Isabelle2013.

Maybe the authors of it can be motivated to brush it up for Isabelle2016
and submit it to AFP, such that it benefits from "automagic" maintenance.

Makarius

Last updated: Apr 20 2024 at 04:19 UTC