The thorn-calculus library contains the Þ-calculus, which is a
general-purpose process calculus. The Þ-calculus is embedded in
Isabelle/HOL, using higher-order abstract syntax (HOAS). The use of HOAS
allows us to have the object language (the Þ-calculus) only deal with
the key features of process calculi, which are concurrency and
communication, and leave the treatment of local names, data,
computation, conditional execution, and repetition to the meta-language
(Isabelle/HOL).
The Þ-calculus strongly resembles the asynchronous π-calculus. Processes communicate via asynchronous channels, which can be global or created locally. Channels are first-class and can therefore be transmitted through other channels, thus making them visible outside their original scopes. This is the mobility feature pioneered by the (synchronous) π-calculus.
You need Isabelle2022 to use this Isabelle library. You can obtain Isabelle2022 from the Isabelle website.
In addition, you need the following Isabelle sessions:
To make this Isabelle library available to your Isabelle installation,
add the path of the src directory to the file
$ISABELLE_HOME_USER/ROOTS. You can find out the value of
$ISABELLE_HOME_USER by running the following command:
isabelle getenv ISABELLE_HOME_USER
Running make builds the PDF file that includes the documentation and
the code and places it in $ISABELLE_BROWSER_INFO/IOG. You can find out
the value of $ISABELLE_BROWSER_INFO by running the following command:
isabelle getenv ISABELLE_BROWSER_INFO
The makefile specifies two targets: properly, which is the default,
and qnd. With properly, fake proofs (sorry) are not accepted; with
qnd, quick-and-dirty mode is used and thus fake proofs are accepted.