Technical reports

A mechanized theory of the π-calculus in HOL

T.F. Melham

January 1992, 31 pages

DOI: 10.48456/tr-244

Abstract

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

@TechReport{UCAM-CL-TR-244,
  author =	 {Melham, T.F.},
  title = 	 {{A mechanized theory of the $\pi$-calculus in HOL}},
  year = 	 1992,
  month = 	 jan,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-244.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-244},
  number = 	 {UCAM-CL-TR-244}
}