Re: [isabelle] Current CSP formalisation with syntax and semantics



On Tue, 3 May 2016, JÃhnig, Nils Erik wrote:

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.

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


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