1. S. Arun-Kumar & Matthew Hennessy (1992): An efficiency preorder for processes. Acta Informatica 29(8), pp. 737–760, doi:10.1007/BF01191894.
  2. Jos C. M. Baeten, Twan Basten & Michel A. Reniers (2010): Process Algebra: Equational Theories of Communicating Processes. Cambridge University Press, doi:10.1017/CBO9781139195003.
  3. Jesper Bengtson (2010): Formalising process calculi. Acta Universitatis Upsaliensis.
  4. Jesper Bengtson & Joachim Parrow (2007): A completeness proof for bisimulation in the pi-calculus using isabelle. Electronic Notes in Theoretical Computer Science 192(1), pp. 61–75, doi:10.1016/j.entcs.2007.08.017.
  5. Kaustuv Chaudhuri, Matteo Cimini & Dale Miller (2015): A lightweight formalization of the metatheory of bisimulation-up-to. In: Proceedings of the 2015 Conference on Certified Programs and Proofs. ACM, pp. 157–166, doi:10.1145/2676724.2693170.
  6. Alonzo Church (1940): A formulation of the simple theory of types. The journal of symbolic logic 5(2), pp. 56–68, doi:10.2307/2266170.
  7. Rance Cleaveland, Joachim Parrow & Bernhard Steffen (1993): The Concurrency Workbench: A semantics-based tool for the verification of concurrent systems. ACM Transactions on Programming Languages and Systems (TOPLAS) 15(1), pp. 36–72, doi:10.1145/151646.151648.
  8. Michael Compton (2005): Embedding a fair CCS in Isabelle/HOL. In: Theorem Proving in Higher Order Logics: Emerging Trends Proceedings, pp. 30, doi: Available at
  9. Adrien Durier, Daniel Hirschkoff & Davide Sangiorgi (2017): Divergence and Unique Solution of Equations. In: Roland Meyer & Uwe Nestmann: 28th International Conference on Concurrency Theory (CONCUR 2017), Leibniz International Proceedings in Informatics (LIPIcs) 85. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, pp. 11:1–11:16, doi:10.4230/LIPIcs.CONCUR.2017.11. Available at
  10. Rob J. van Glabbeek (2005): A characterisation of weak bisimulation congruence. In: Processes, Terms and Cycles: Steps on the Road to Infinity. Springer, pp. 26–39, doi:10.1007/11601548_4.
  11. Michael J. C. Gordon, Arthur J. Milner & Christopher P. Wadsworth (1979): Edinburgh LCF: A Mechanised Logic of Computation. Lecture Notes in Computer Science 78. Springer, Berlin Heidelberg, doi:10.1007/3-540-09724-4.
  12. Roberto Gorrieri (2017): CCS (25, 12) is Turing-complete. Fundamenta Informaticae 154(1-4), pp. 145–166, doi:10.3233/FI-2017-1557.
  13. Roberto Gorrieri & Cristian Versari (2015): Introduction to Concurrency Theory. Transition Systems and CCS. Springer, Cham, doi:10.1007/978-3-319-21491-7.
  14. Daniel Hirschkoff (1997): A full formalisation of π-calculus theory in the calculus of constructions. In: International Conference on Theorem Proving in Higher Order Logics. Springer, pp. 153–169, doi:10.1007/BFb0028392.
  15. HOL4 contributors (2018): The HOL System DESCRIPTION. Available at
  16. HOL4 contributors (2018): The HOL System LOGIC. Available at
  17. Temesghen Kahsai & Marino Miculan (2008): Implementing spi calculus using nominal techniques. In: Conference on Computability in Europe. Springer, pp. 294–305, doi:10.1007/978-3-540-69407-6_33.
  18. Joe Leslie-Hurd (2011): The OpenTheory standard theory library. In: NASA Formal Methods Symposium. Springer, pp. 177–191, doi:10.1007/978-3-642-20398-5_14.
  19. Thomas F. Melham (1992): The HOL pred_sets Library. Universiy of Cambridge Computer Lab, doi: Available at
  20. Thomas F. Melham (1994): A Mechanized Theory of the Pi-Calculus in HOL. Nord. J. Comput. 1(1), pp. 50–76, doi: Available at
  21. Robin Milner (1972): Logic for Computable Functions: description of a machine implementation. Technical Report. STANFORD UNIV CA DEPT OF COMPUTER SCIENCE. Available at
  22. Robin Milner (1989): Communication and concurrency. PHI Series in computer science. Prentice-Hall.
  23. Otmane Aït Mohamed (1995): Mechanizing a π-calculus equivalence in HOL. In: International Conference on Theorem Proving in Higher Order Logics. Springer, pp. 1–16, doi:10.1007/3-540-60275-5_53.
  24. Monica Nesi (1992): A formalization of the process algebra CCS in high order logic. Technical Report UCAM-CL-TR-278. University of Cambridge, Computer Laboratory. Available at
  25. Monica Nesi (1999): Formalising a Value-Passing Calculus in HOL. Formal Aspects of Computing 11(2), pp. 160–199, doi:10.1007/s001650050046.
  26. Michael Norrish & Brian Huffman (2013): Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω_1. In: International Conference on Interactive Theorem Proving. Springer, pp. 133–146, doi:10.1007/978-3-642-39634-2_12.
  27. Joachim Parrow & Jesper Bengtson (2009): Formalising the pi-calculus using nominal logic. Logical Methods in Computer Science 5, doi:10.2168/LMCS-5(2:16)2009.
  28. Damien Pous (2007): New up-to techniques for weak bisimulation. Theoretical Computer Science 380, pp. 164–180, doi:10.1016/j.tcs.2007.02.060.
  29. Andrew W. Roscoe (1998): The theory and practice of concurrency. Prentice Hall. Available at
  30. Andrew W. Roscoe (2010): Understanding Concurrent Systems. Springer, doi:10.1007/978-1-84882-258-0.
  31. Davide Sangiorgi (2011): Introduction to Bisimulation and Coinduction. Cambridge University Press, doi:10.1017/CBO9780511777110.
  32. Davide Sangiorgi (2015): Equations, contractions, and unique solutions. In: ACM SIGPLAN Notices 50. ACM, pp. 421–432, doi:10.1145/2676726.2676965. Available at
  33. Davide Sangiorgi (2017): Equations, contractions, and unique solutions. ACM Transactions on Computational Logic (TOCL) 18, pp. 4, doi:10.1145/2971339. Available at
  34. Davide Sangiorgi & Robin Milner (1992): The problem of Weak Bisimulation up to. In: International Conference on Concurrency Theory. Springer, pp. 32–46, doi:10.1007/BFb0084781. Available at
  35. Davide Sangiorgi & Jan Rutten (2011): Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, doi:10.1017/CBO9780511777110.
  36. Konrad Slind & Michael Norrish (2008): A brief overview of HOL4. In: International Conference on Theorem Proving in Higher Order Logics. Springer, pp. 28–32, doi:10.1007/978-3-540-71067-7_6. Available at
  37. Chun Tian (2017): A Formalization of Unique Solutions of Equations in Process Algebra. AlmaDigital, Bologna. Available at

Comments and questions to:
For website issues: