A Formal Semantics and an Interactive Environment for Sisal

We present a formal definition of the dynamic semantics of a significant part of the language Sisal 2.0 in the structural operational style of Natural Semantics, using Typol inference rules within the Centaur system, a generic specification environment. Sisal is a strongly typed, applicative, single assignment language in use on a variety of parallel processors, including conventional multiprocessors, vector machines and data-flow machines.The motivations of our work are, with a formal semantic description of Sisal, to provide a firm foundation for understanding and evaluating language design issues, aid the elimination of ambiguities in the language, and provide a valuable reference for both implementors and programmers. At the same time, Centaur specifications automatically yield a structure editor and an interpreter for Sisal, which can be developed into an interactive environment for Sisal programming. Besides classical dynamic semantic aspects of functional programming languages such as the absence of side-effects and aliasing, the notion of referential transparency, and higher-order functions, we have characterized specific semantic aspects of the Sisal language such as arrays, infinite streams, sequential and parallel loops.From this semantic definition, we intend to formally define program transformations, particularly parallelization techniques and algorithms for Sisal compilation, and to incorporate such techniques into a program development and visualization environment for Sisal programming.