Department of Computer Science and Technology

Technical reports

A complete proof system for SCCS with model assertions

Glynn Winskel

September 1985, 23 pages

DOI: 10.48456/tr-78

Abstract

This paper presents a proof system for Robin Milner’s Synchronous Calculus of Communicating Systems (SCCS) with modal assertions. The language of assertions is a fragment of dynamic logic, sometimes called Hennessy-Milner logic after they brought it to attention; while rather weak from a practical point of view, its assertions are expressive enough to characterise observation equivalence, central to the work of Milner et al. on CCS and SCCS. The paper includes a completeness result and a proof of equivalence between an operational and denotational semantics for SCCS. Its emphasis is on the theoretical issues involved in the construction of proof systems for parallel programming langauges.

Full text

PDF (1.0 MB)

BibTeX record

@TechReport{UCAM-CL-TR-78,
  author =	 {Winskel, Glynn},
  title = 	 {{A complete proof system for SCCS with model assertions}},
  year = 	 1985,
  month = 	 sep,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-78.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-78},
  number = 	 {UCAM-CL-TR-78}
}