An operational semantics for skeletons

A major weakness of the current programming systems based on skeletons is that parallel semantics is usually provided in an informal way, thus preventing any formal comparison about program behavior. We describe a schema suitable for the description of both functional and parallel semantics of skeletal languages which is aimed at filling this gap. The proposed schema of semantics represents a handy framework to prove the correctness and validate different rewriting rules. These can be used to transform a skeleton program into a functionally equivalent but possibly faster version.