, on sums, the result is similar to Milner's original 'unique solution of equations' theorem for strong bisimilarity (?)-the same weakly guarded context (WG) is required
, Milner's "unique solution of equations" theorem for rooted bisimilarity (? c ) has more severe constraints (must be both strongly guarded and sequential
,
, 9]) for automatically proving bisimilarities of CCS processes. Her work is the working basis of ours. However, the differences are substantial, especially in the way of defining bisimilarities. We greatly benefited from features and standard libraries in recent versions of HOL4, Monica Nesi did the first CCS formalisations for both pure and value-passing CCS, vol.24
, Weber did a substantial formalisation work on CCS, ?-calculi and ?-calculi using Isabelle/HOL and its nominal logic
, Abella, the latter focuses on 'bisimulation up-to' techniques for CCS and ?-calculus. Damien Pous [28] also formalised up-to techniques and some CCS examples in Coq. Formalisations less related to ours include Kahsai and Miculan, vol.7
, The HOL System DESCRIPTION. Available at, 2018.
, The HOL System LOGIC. Available at, 2018.
, An efficiency preorder for processes, Acta Informatica, vol.29, issue.8, pp.737-760, 1992.
, Process Algebra: Equational Theories of Communicating Processes, 2010.
, Formalising process calculi, 2010.
, A completeness proof for bisimulation in the picalculus using isabelle, Electronic Notes in Theoretical Computer Science, vol.192, issue.1, pp.61-75, 2007.
, A lightweight formalization of the metatheory of bisimulation-up-to, Proceedings of the 2015 Conference on Certified Programs and Proofs, ACM, pp.157-166, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01091524
, A formulation of the simple theory of types, The journal of symbolic logic, vol.5, issue.2, pp.56-68, 1940.
, The Concurrency Workbench: A semantics-based tool for the verification of concurrent systems, ACM Transactions on Programming Languages and Systems, vol.15, issue.1, pp.36-72, 1993.
, Theorem Proving in Higher Order Logics: Emerging Trends Proceedings, p.30, 2005.
, Divergence and Unique Solution of Equations, Leibniz International Proceedings in Informatics (LIPIcs) 85, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, vol.11, p.16, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01643502
, A characterisation of weak bisimulation congruence, Processes, Terms and Cycles: Steps on the Road to Infinity, pp.26-39, 2005.
, Edinburgh LCF: A Mechanised Logic of Computation, Lecture Notes in Computer Science, vol.78, 1979.
, CCS (25, 12) is Turing-complete, Fundamenta Informaticae, vol.154, issue.1-4, pp.145-166, 2017.
DOI : 10.3233/fi-2017-1557
, Introduction to Concurrency Theory. Transition Systems and CCS, 2015.
, A full formalisation of ?-calculus theory in the calculus of constructions, International Conference on Theorem Proving in Higher Order Logics, pp.153-169, 1997.
, The OpenTheory standard theory library, NASA Formal Methods Symposium, pp.177-191, 2011.
DOI : 10.1007/978-3-642-20398-5_14
URL : http://www.gilith.com/research/papers/stdlib.pdf
, Implementing spi calculus using nominal techniques, Conference on Computability in Europe, pp.294-305, 2008.
, The HOL pred_sets Library, 1992.
, A Mechanized Theory of the Pi-Calculus in HOL, Nord. J. Comput, vol.1, issue.1, pp.50-76, 1994.
, Logic for Computable Functions: description of a machine implementation, 1972.
DOI : 10.21236/ad0785072
URL : http://www.dtic.mil/dtic/tr/fulltext/u2/785072.pdf
, Communication and concurrency. PHI Series in computer science, 1989.
, Mechanizing a ?-calculus equivalence in HOL, International Conference on Theorem Proving in Higher Order Logics, pp.1-16, 1995.
, A formalization of the process algebra CCS in high order logic, 1992.
, Formalising a Value-Passing Calculus in HOL, Formal Aspects of Computing, vol.11, issue.2, pp.160-199, 1999.
DOI : 10.1007/s001650050046
, Ordinals in HOL: Transfinite arithmetic up to (and beyond) ? 1, International Conference on Interactive Theorem Proving, pp.133-146, 2013.
, Formalising the pi-calculus using nominal logic, Logical Methods in Computer Science, vol.5, 2009.
DOI : 10.2168/lmcs-5(2:16)2009
URL : https://lmcs.episciences.org/832/pdf
, New up-to techniques for weak bisimulation, Theoretical Computer Science, vol.380, pp.164-180, 2007.
DOI : 10.1016/j.tcs.2007.02.060
URL : https://hal.archives-ouvertes.fr/hal-01442745
, The theory and practice of concurrency, 1998.
, Understanding Concurrent Systems, 2010.
DOI : 10.1007/978-1-84882-258-0
, Introduction to Bisimulation and Coinduction, 2011.
DOI : 10.1017/cbo9780511777110
URL : https://hal.archives-ouvertes.fr/hal-00907026
, Equations, contractions, and unique solutions, vol.50, pp.421-432, 2015.
DOI : 10.1145/2775051.2676965
URL : https://hal.archives-ouvertes.fr/hal-01089205
, Equations, contractions, and unique solutions, ACM Transactions on Computational Logic (TOCL), vol.18, p.4, 2017.
DOI : 10.1145/2775051.2676965
URL : https://hal.archives-ouvertes.fr/hal-01089205
, The problem of "Weak Bisimulation up to, International Conference on Concurrency Theory, pp.32-46, 1992.
, Advanced Topics in Bisimulation and Coinduction, 2011.
, A brief overview of HOL4, International Conference on Theorem Proving in Higher Order Logics, pp.28-32, 2008.
, A Formalization of Unique Solutions of Equations in Process Algebra, 2017.