Department of Computer Science and Technology

Technical reports

A mechanized theory of the π-calculus in HOL

T.F. Melham

January 1992, 31 pages

DOI: 10.48456/tr-244


The π-calculus is a process algebra developed at Edinburgh by Milner, Parrow and Walker for modelling concurrent systems in which the pattern of communication between processes may change over time. This paper describes the results of preliminary work on a mechanized formal theory of the π-calculus in higher order logic using the HOL theorem prover.

Full text

PDF (2.0 MB)

BibTeX record

  author =	 {Melham, T.F.},
  title = 	 {{A mechanized theory of the $\pi$-calculus in HOL}},
  year = 	 1992,
  month = 	 jan,
  url = 	 {},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-244},
  number = 	 {UCAM-CL-TR-244}