| We study the use of abstraction to reason operationally about concurrent programs. Our thesis is that abstraction can profitably be combined with operational semantics to produce new proof techniques. We study two very different applications: (1) the implementation of nested data-parallelism, and (2) the verification of value-passing processes.; In the first case, we develop a typing system for a nested data-parallel programming language and use it to prove the correctness of flattening, an important compilation technique. In the second, we demonstrate that abstract interpretations of values domains can be applied to process description languages, extending the applicability of finite-state methods to infinite-state processes. |
