Partial evaluation scheme for concurrent languages and its correctness

Abstract

A simple, general, and well-formalized partial evaluation method for concurrent languages is proposed. In spite of many potential benefits, there are few partial evaluation techniques for concurrent languages. We choose a process calculus for the target language because it has theoretical clarity, and yet has expressive power enough to represent various high-level constructs in concurrent object-oriented languages. We realize effective optimization by allowing elimination of even nondeterministic interprocess communications. Furthermore, we prove correctness of our method with respect to barb-agreed simulation.