Towards a formal semantics of paraML
Peter Bailey
Department of Computer Science,
The Australian National University,
Canberra ACT 0200, Australia.
Peter.Bailey@cs.anu.edu.au
Abstract
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