A fully abstract semantics for a concurrent functional language with monadic types
Alan Jeffrey · 2002
This paper presents a typed higher-order concurrent functional programming language, based on Moggi's monadic metalanguage and Reppy's Concurrent ML. We present an operational semantics for the language, and show that a higher-order variant of the traces model is fully abstract for may-testing. This proof uses a program logic based on Hennessy-Milner logic and Abramsky's domain theory in logical form.