Formalizing CORRELATE - from Practice to Pi

Correlate is a concurrent object-oriented language that has been used in real-world applications in areas of High- Performance Computing, network applications and multi-agent systems. The practical goal of the language is to offer a powerful programming environment in which both application and system software can be described using the paradigm of concurrent objects. In this paper, the formal description of Correlate in the pi-calculus is discussed. In our experience, such a formalization process is a crucial step in the design process of a practical language, even though not every detail need to be modelled. Several examples illustrate the benefits of our specification especially from the viewpoint of the language designer. Finally it is shown that an operational prototype can be easily constructed by translation from the pi-calculus to Pict.