A Semantics for ML Concurrency Primitives

Dave Berry; Robin Milner; David N. Turner

doi:10.1145/143165.143191

A Semantics for ML Concurrency Primitives

Dave Berry, Robin Milner, David N. Turner

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

We present a set of concurrency primitives for Standard ML. We define these by giving the transitional semantics of a simple language. We prove that our semantics preserves the expected behaviour of sequential programs. We also show that we can define stores as processes, such that the representation has the same behaviour as a direct definition. These proofs are the first steps towards integrating our semantics with the full definition of Standard ML.

Original language	English
Title of host publication	POPL '92 Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages
Pages	119-129
Number of pages	11
DOIs	https://doi.org/10.1145/143165.143191
Publication status	Published - Feb 1992

Access to Document

10.1145/143165.143191

http://dl.acm.org/citation.cfm?doid=143165.143191

Cite this

@inproceedings{66a57c8577564135803a1a5a34595e10,

title = "A Semantics for ML Concurrency Primitives",

abstract = "We present a set of concurrency primitives for Standard ML. We define these by giving the transitional semantics of a simple language. We prove that our semantics preserves the expected behaviour of sequential programs. We also show that we can define stores as processes, such that the representation has the same behaviour as a direct definition. These proofs are the first steps towards integrating our semantics with the full definition of Standard ML. ",

author = "Dave Berry and Robin Milner and Turner, {David N.}",

year = "1992",

month = feb,

doi = "10.1145/143165.143191",

language = "English",

isbn = "0-89791-453-8",

pages = "119--129",

booktitle = "POPL '92 Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages",

}

TY - GEN

T1 - A Semantics for ML Concurrency Primitives

AU - Berry, Dave

AU - Milner, Robin

AU - Turner, David N.

PY - 1992/2

Y1 - 1992/2

N2 - We present a set of concurrency primitives for Standard ML. We define these by giving the transitional semantics of a simple language. We prove that our semantics preserves the expected behaviour of sequential programs. We also show that we can define stores as processes, such that the representation has the same behaviour as a direct definition. These proofs are the first steps towards integrating our semantics with the full definition of Standard ML.

AB - We present a set of concurrency primitives for Standard ML. We define these by giving the transitional semantics of a simple language. We prove that our semantics preserves the expected behaviour of sequential programs. We also show that we can define stores as processes, such that the representation has the same behaviour as a direct definition. These proofs are the first steps towards integrating our semantics with the full definition of Standard ML.

U2 - 10.1145/143165.143191

DO - 10.1145/143165.143191

M3 - Conference contribution

SN - 0-89791-453-8

SP - 119

EP - 129

BT - POPL '92 Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

ER -

A Semantics for ML Concurrency Primitives

Abstract

Access to Document

Fingerprint

Cite this