@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/},
)