Full Abstractness for a Functional/Concurrent Language with Higher-Order Value-Passing

AbstractWe study an applied typed call-by-valueλ-calculus which in addition to the usual types for higher-order functions contains an extra type called proc, for processes; the constructors for terms of this type are similar to those found in standard process calculi such as CCS. We first give an operational semantics for this language in terms of a labeled transition system which is then used to give a behavioral preorder based on contexts; the expressionNdominatesMif in every appropriate context ifMcan produce a boolean value then so canN. Based on standard domain constructors we define a model, a prime algebraic lattice, which isfully abstractwith respect to this behavior preorder; expressions are related in the model if and only if they are related behaviorally. The proof method uses concepts that are of independent interest. It involves characterizing the domain using filters of a property logic for program expressions and developing a program logic for relating program expressions with property formulae