Abstract A substantial amount of work has been devoted to the proof of correctness of various program analyses but much less attention has been paid to the correctness of compiler optimisations based on these analyses. In this paper we tackle the problem in the context of strictness analysis for lazy functional languages. We show that compiler optimisations based on strictness analysis can be expressed formally in the functional framework using continuations. This formal presentation has two benefits: it allows us to give a rigorous correctness proof of the optimised compiler; and it exposes the various optimisations made possible by a strictness analysis.

Abstract Distributed implementations of programming languages with implicit parallelism hold out the prospect that the parallel programs are immediately scalable. This paper presents some of the results of our part of Esprit 415, in which we considered the implementation of lazy functional programming languages on distributed architectures. A compiler and abstract machine were designed to achieve this goal. The abstract parallel machine was formally specified, using Miranda. Each instruction of the abstract machine was then implemented as a macro in the Transputer Assembler. Although macro expansion of the code results in non-optimal code generation, use of the Miranda specification makes it possible to validate the compiler before the Transputer code is generated. The hardware currently available consists of five T800-25s, each board having 16 Mbytes of memory. Benchmark timings using this hardware are given. In spite of the straightforward code-generation, the resulting system compares favourably with more sophisticated sequential implementations, such as that of LML.

Abstract The evaluation transformer model of reduction generalizes lazy evaluation in two ways: it can start the evaluation of expressions before their first use, and it can evaluate expressions further than weak head normal form. Moreover, the amount of evaluation required of an argument to a function may depend on the amount of evaluation required of the function application. It is a suitable candidate model for implementing lazy functional languages on parallel machines. In this paper we explore the implementation of lazy functional languages on parallel machines, both shared and distributed memory architectures, using the evaluation transformer model of reduction. We will see that the same code can be produced for both styles of architecture, and the definition of the instruction set is virtually the same for each style. The essential difference is that a distributed memory architecture has one extra node type for non-local pointers, and instructions which involve the value of such nodes need their definitions extended to cover this new type of node. To make our presentation accessible, we base our description on a variant of the well-known G-machine, an abstract machine for executing lazy functional programs.

Abstract interpretation and projection analysis are two techniques for finding out information about lazy functional programs. Two typical uses of these techniques are speeding up sequential implementations, and the introduction of parallelism into parallel implementations.

Many models for the parallel reduction of lazy functional languages have been proposed in the literature. The one we have chosen to implement is based on evaluation transformers. An evaluation transformer says how much evaluation can be done to an argument expression in a function application, given the amount of evaluation that can be done to the application. Rather than just selecting a distributed memory architecture and trying to support parallel graph reduction, we investigate the implications of a minimally specified distributed memory architecture for parallel graph reduction. The results of the investigation are incorporated into an abstract machine which is able to support the communication and synchronisation needs of the parallel reduction model on a distributed memory architecture. Certain flags are needed on the nodes in the program graph in order to support the model. These are motivated and described.