Towards a formal semantics of paraML

Peter Bailey
Department of Computer Science, The Australian National University, Canberra ACT 0200, Australia.


The original design and implementation of paraML, a parallel extension to Standard ML, was an organic exercise in language development, responding to the suggestions of users and addressing performance limitations. A complete redesign of the language extensions has taken place over the last year. In contrast to the previous experiment, the redesign has taken place simultaneously with the development of a formal semantics for the extensions. The implementation of the new language is in progress, and has been simplified by the semantic separation of core and derived extensions. The semantics define a lambda calculus with rules for sequential and parallel evaluation. The core extensions of paraML are defined by the parallel evaluation rules, which describe how processes and communication ports are created, and how values are passed from processes to ports. Further work is required to develop an appropriate model of evaluation traces and properties of the configurations of processes, and to prove the type soundness of the calculus.
Conference Home Page