@article(arun1992efficiency,
 author       = {Arun-Kumar, S. and Matthew Hennessy},
 year         = {1992},
 title        = {An efficiency preorder for processes},
 journal      = {Acta Informatica},
 volume       = {29},
 number       = {8},
 pages        = {737--760},
 doi          = {10.1007/BF01191894},
)
@book(BaeBOOK,
 author       = {Jos C. M. Baeten and Twan Basten and Michel A. Reniers},
 year         = {2010},
 title        = {Process Algebra: Equational Theories of Communicating Processes},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139195003},
)
@phdthesis(bengtson2010formalising,
 author       = {Jesper Bengtson},
 year         = {2010},
 title        = {Formalising process calculi},
 school       = {Acta Universitatis Upsaliensis},
)
@article(bengtson2007completeness,
 author       = {Jesper Bengtson and Joachim Parrow},
 year         = {2007},
 title        = {A completeness proof for bisimulation in the pi-calculus using isabelle},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {192},
 number       = {1},
 pages        = {61--75},
 doi          = {10.1016/j.entcs.2007.08.017},
)
@inproceedings(chaudhuri2015lightweight,
 author       = {Kaustuv Chaudhuri and Matteo Cimini and Dale Miller},
 year         = {2015},
 title        = {A lightweight formalization of the metatheory of bisimulation-up-to},
 booktitle    = {Proceedings of the 2015 Conference on Certified Programs and Proofs},
 organization = {ACM},
 pages        = {157--166},
 doi          = {10.1145/2676724.2693170},
)
@article(church1940formulation,
 author       = {Alonzo Church},
 year         = {1940},
 title        = {A formulation of the simple theory of types},
 journal      = {The journal of symbolic logic},
 volume       = {5},
 number       = {2},
 pages        = {56--68},
 doi          = {10.2307/2266170},
)
@article(cleaveland1993concurrency,
 author       = {Rance Cleaveland and Joachim Parrow and Bernhard Steffen},
 year         = {1993},
 title        = {The Concurrency Workbench: A semantics-based tool for the verification of concurrent systems},
 journal      = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
 volume       = {15},
 number       = {1},
 pages        = {36--72},
 doi          = {10.1145/151646.151648},
)
@inproceedings(compton2005embedding,
 author       = {Michael Compton},
 year         = {2005},
 title        = {Embedding a fair CCS in Isabelle/HOL},
 booktitle    = {Theorem Proving in Higher Order Logics: Emerging Trends Proceedings},
 pages        = {30},
 doi          = {10.1.1.105.834},
 url          = {https://web.comlab.ox.ac.uk/techreports/oucl/RR-05-02.pdf#page=36},
)
@inproceedings(DurierHS17,
 author       = {Adrien Durier and Daniel Hirschkoff and Davide Sangiorgi},
 year         = {2017},
 title        = {{Divergence and Unique Solution of Equations}},
 editor       = {Roland Meyer and Uwe Nestmann},
 booktitle    = {28th International Conference on Concurrency Theory (CONCUR 2017)},
 series       = {Leibniz International Proceedings in Informatics (LIPIcs)},
 volume       = {85},
 publisher    = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
 address      = {Dagstuhl, Germany},
 pages        = {11:1--11:16},
 doi          = {10.4230/LIPIcs.CONCUR.2017.11},
 url          = {http://drops.dagstuhl.de/opus/volltexte/2017/7784},
)
@inproceedings(van2005characterisation,
 author       = {Rob J. van Glabbeek},
 year         = {2005},
 title        = {A characterisation of weak bisimulation congruence},
 booktitle    = {Processes, Terms and Cycles: Steps on the Road to Infinity},
 publisher    = {Springer},
 pages        = {26--39},
 doi          = {10.1007/11601548_4},
)
@book(gordon1979edinburgh,
 author       = {Michael J. C. Gordon and Arthur J. Milner and Christopher P. Wadsworth},
 year         = {1979},
 title        = {Edinburgh {LCF}: A Mechanised Logic of Computation},
 series       = {Lecture Notes in Computer Science},
 volume       = {78},
 publisher    = {Springer},
 address      = {Berlin Heidelberg},
 doi          = {10.1007/3-540-09724-4},
)
@article(gorrieri2017ccs,
 author       = {Roberto Gorrieri},
 year         = {2017},
 title        = {CCS (25, 12) is Turing-complete},
 journal      = {Fundamenta Informaticae},
 volume       = {154},
 number       = {1-4},
 pages        = {145--166},
 doi          = {10.3233/FI-2017-1557},
)
@book(Gorrieri:2015jt,
 author       = {Roberto Gorrieri and Cristian Versari},
 year         = {2015},
 title        = {{Introduction to Concurrency Theory}},
 series       = {Transition Systems and CCS},
 publisher    = {Springer},
 address      = {Cham},
 doi          = {10.1007/978-3-319-21491-7},
)
@inproceedings(hirschkoff1997full,
 author       = {Daniel Hirschkoff},
 year         = {1997},
 title        = {A full formalisation of $\pi$-calculus theory in the calculus of constructions},
 booktitle    = {International Conference on Theorem Proving in Higher Order Logics},
 organization = {Springer},
 pages        = {153--169},
 doi          = {10.1007/BFb0028392},
)
@manual(holdesc,
 author       = {{HOL4 contributors}},
 year         = {2018},
 title        = {{The HOL System DESCRIPTION}},
 url          = {http://sourceforge.net/projects/hol/files/hol/kananaskis-12/kananaskis-12-description.pdf},
)
@manual(hollogic,
 author       = {{HOL4 contributors}},
 year         = {2018},
 title        = {{The HOL System LOGIC}},
 url          = {http://sourceforge.net/projects/hol/files/hol/kananaskis-12/kananaskis-12-logic.pdf},
)
@inproceedings(kahsai2008implementing,
 author       = {Temesghen Kahsai and Marino Miculan},
 year         = {2008},
 title        = {Implementing spi calculus using nominal techniques},
 booktitle    = {Conference on Computability in Europe},
 organization = {Springer},
 pages        = {294--305},
 doi          = {10.1007/978-3-540-69407-6_33},
)
@inproceedings(hurd2011opentheory,
 author       = {Leslie-Hurd, Joe},
 year         = {2011},
 title        = {The OpenTheory standard theory library},
 booktitle    = {NASA Formal Methods Symposium},
 organization = {Springer},
 pages        = {177--191},
 doi          = {10.1007/978-3-642-20398-5_14},
)
@article(melham1992hol,
 author       = {Thomas F. Melham},
 year         = {1992},
 title        = {The HOL pred_sets Library},
 journal      = {Universiy of Cambridge Computer Lab},
 doi          = {10.1.1.219.5390},
 url          = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.219.5390},
)
@article(melham1994mechanized,
 author       = {Thomas F. Melham},
 year         = {1994},
 title        = {A Mechanized Theory of the Pi-Calculus in HOL},
 journal      = {Nord. J. Comput.},
 volume       = {1},
 number       = {1},
 pages        = {50--76},
 doi          = {10.1.1.56.4370},
 url          = {http://core.ac.uk/download/pdf/22878407.pdf},
)
@techreport(milner1972logic,
 author       = {Robin Milner},
 year         = {1972},
 title        = {Logic for Computable Functions: description of a machine implementation},
 type         = {Technical Report},
 institution  = {STANFORD UNIV CA DEPT OF COMPUTER SCIENCE},
 url          = {http://www.dtic.mil/dtic/tr/fulltext/u2/785072.pdf},
)
@book(Mil89,
 author       = {Robin Milner},
 year         = {1989},
 title        = {{Communication and concurrency}},
 series       = {{PHI} Series in computer science},
 publisher    = {Prentice-Hall},
)
@inproceedings(mohamed1995mechanizing,
 author       = {Otmane A{\"\i}t Mohamed},
 year         = {1995},
 title        = {Mechanizing a $\pi$-calculus equivalence in HOL},
 booktitle    = {International Conference on Theorem Proving in Higher Order Logics},
 organization = {Springer},
 pages        = {1--16},
 doi          = {10.1007/3-540-60275-5_53},
)
@techreport(Nesi:1992ve,
 author       = {Monica Nesi},
 year         = {1992},
 title        = {{A formalization of the process algebra CCS in high order logic}},
 type         = {Technical Report},
 number       = {UCAM-CL-TR-278},
 institution  = {University of Cambridge, Computer Laboratory},
 url          = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-278.pdf},
)
@article(Nesi:2017wo,
 author       = {Monica Nesi},
 year         = {1999},
 title        = {{Formalising a Value-Passing Calculus in HOL}},
 journal      = {Formal Aspects of Computing},
 volume       = {11},
 number       = {2},
 pages        = {160--199},
 doi          = {10.1007/s001650050046},
)
@inproceedings(norrish2013ordinals,
 author       = {Michael Norrish and Brian Huffman},
 year         = {2013},
 title        = {{Ordinals in HOL: Transfinite arithmetic up to (and beyond) $\omega_1$}},
 booktitle    = {International Conference on Interactive Theorem Proving},
 organization = {Springer},
 pages        = {133--146},
 doi          = {10.1007/978-3-642-39634-2_12},
)
@article(parrow2009formalising,
 author       = {Joachim Parrow and Jesper Bengtson},
 year         = {2009},
 title        = {Formalising the pi-calculus using nominal logic},
 journal      = {Logical Methods in Computer Science},
 volume       = {5},
 doi          = {10.2168/LMCS-5(2:16)2009},
)
@article(pous2007new,
 author       = {Damien Pous},
 year         = {2007},
 title        = {New up-to techniques for weak bisimulation},
 journal      = {Theoretical Computer Science},
 volume       = {380},
 pages        = {164--180},
 doi          = {10.1016/j.tcs.2007.02.060},
)
@book(theoryAndPractice,
 author       = {Andrew W. Roscoe},
 year         = {1998},
 title        = {The theory and practice of concurrency},
 publisher    = {{Prentice Hall}},
 url          = {http://www.cs.ox.ac.uk/people/bill.roscoe/publications/68b.pdf},
)
@book(RosUnder10,
 author       = {Andrew W. Roscoe},
 year         = {2010},
 title        = {Understanding Concurrent Systems},
 publisher    = {Springer},
 doi          = {10.1007/978-1-84882-258-0},
)
@book(Sangiorgi:2011ut,
 author       = {Davide Sangiorgi},
 year         = {2011},
 title        = {Introduction to Bisimulation and Coinduction},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511777110},
)
@inproceedings(sangiorgi2015equations,
 author       = {Davide Sangiorgi},
 year         = {2015},
 title        = {Equations, contractions, and unique solutions},
 booktitle    = {ACM SIGPLAN Notices},
 volume       = {50},
 organization = {ACM},
 pages        = {421--432},
 doi          = {10.1145/2676726.2676965},
 url          = {https://hal.inria.fr/hal-01089205},
)
@article(sangiorgi2017equations,
 author       = {Davide Sangiorgi},
 year         = {2017},
 title        = {Equations, contractions, and unique solutions},
 journal      = {ACM Transactions on Computational Logic (TOCL)},
 volume       = {18},
 pages        = {4},
 doi          = {10.1145/2971339},
 url          = {https://hal.inria.fr/hal-01647063},
)
@inproceedings(sangiorgi1992problem,
 author       = {Davide Sangiorgi and Robin Milner},
 year         = {1992},
 title        = {The problem of \IeC{\textquotedblleft}Weak Bisimulation up to\IeC{\textquotedblright}},
 booktitle    = {International Conference on Concurrency Theory},
 organization = {Springer},
 pages        = {32--46},
 doi          = {10.1007/BFb0084781},
 url          = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.5964},
)
@book(sangiorgi2011advanced,
 author       = {Davide Sangiorgi and Jan Rutten},
 year         = {2011},
 title        = {Advanced Topics in Bisimulation and Coinduction},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511777110},
)
@inproceedings(slind2008brief,
 author       = {Konrad Slind and Michael Norrish},
 year         = {2008},
 title        = {A brief overview of HOL4},
 booktitle    = {International Conference on Theorem Proving in Higher Order Logics},
 organization = {Springer},
 pages        = {28--32},
 doi          = {10.1007/978-3-540-71067-7_6},
 url          = {http://ts.data61.csiro.au/publications/nicta_full_text/1482.pdf},
)
@mastersthesis(Tian:2017wrba,
 author       = {Chun Tian},
 year         = {2017},
 title        = {{A Formalization of Unique Solutions of Equations in Process Algebra}},
 school       = {AlmaDigital},
 address      = {Bologna},
 url          = {http://amslaurea.unibo.it/14798/},
)