Technical reports

A concurrent object calculus:
reduction and typing

Andrew D. Gordon, Paul D. Hankin

February 1999, 63 pages

DOI: 10.48456/tr-457

Abstract

We obtain a new formalism for concurrent object-oriented languages by extending Abadi abd Cardelli’s imperative object calculus with operators for concurrency from the μ-calculus and with operators for synchronisation based on mutexes. Our syntax of terms is extremely expressive; in a precise sense it unifies notions of expression, process, store, thread and configuration. We present a chemical-style reduction semantics, and prove it equivalent to a structural operational semantics. We identify a deterministic fragment that is closed under reduction and show that it includes the imperative object calculus. A collection of type systems for object oriented constructs is at the heart of Abadi and Cardelli’s work. We recast one of Abadi and Cardelli’s first-order type systems with object types and subtyping in the setting of our calculus and prove subject reduction. Since our syntax of terms includes both stores and running expressions, we avoid the need to separate store typing from typing of expressions. We translate communication channels and choice-free asynchronous μ-calculus into our calculus to illustrate its expressiveness; the types of read-only and write-only channels are supertypes of read-write channels.

Full text

PDF (3.3 MB)

BibTeX record

@TechReport{UCAM-CL-TR-457,
  author =	 {Gordon, Andrew D. and Hankin, Paul D.},
  title = 	 {{A concurrent object calculus: reduction and typing}},
  year = 	 1999,
  month = 	 feb,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-457.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-457},
  number = 	 {UCAM-CL-TR-457}
}