Full Abstraction for HOPLA

Mikkel Nygaard
Glynn Winskel

December 2003

Abstract:

A fully abstract denotational semantics for the higher-order process language HOPLA is presented. It characterises contextual and logical equivalence, the latter linking up with simulation. The semantics is a clean, domain-theoretic description of processes as downwards-closed sets of computation paths: the operations of HOPLA arise as syntactic encodings of canonical constructions on such sets; full abstraction is a direct consequence of expressiveness with respect to computation paths; and simple proofs of soundness and adequacy shows correspondence between the denotational and operational semantics.

Available as PostScript, PDF, DVI.

 

Last modified: 2004-01-23 by webmaster.