Merge enhancement/readme-completion of pull request #133 into master

jeltsch · jeltsch · commit c6e9c5ea66ce · 2024-01-23T01:22:37.000+02:00
Complete `README.md`
diff --git a/README.md b/README.md
@@ -1,7 +1,21 @@
 Overview
 ========
 
-[…]
+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.
 
 
 Requirements
@@ -14,6 +28,12 @@ Isabelle2022 from the [Isabelle website][isabelle].
     https://isabelle.in.tum.de/
     "Isabelle"
 
+In addition, you need the following Isabelle sessions:
+
+  * [`ZFC_in_HOL`](https://www.isa-afp.org/entries/ZFC_in_HOL.html)
+  * [`Equivalence_Reasoner`](https://github.com/input-output-hk/equivalence-reasoner)
+  * [`Transition_Systems`](https://github.com/input-output-hk/transition-systems)
+
 
 Setup
 =====
