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.
|Title of host publication||POPL '92 Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages|
|Number of pages||11|
|Publication status||Published - Feb 1992|