My PhD thesis is available online, via my WWW page . or via anonymous ftp .
Abstract
The goal of my thesis is to extend current methods for compiler derivation and verification to languages which exhibit true concurrency. The work has proceeded through the following steps.
A process calculus, called CLAM, was defined, based on the lambda-calculus and modelling true concurrency. CLAM was used to define the semantics of a simple concurrent functional language, called Urlang, which was inspired by the programming language Erlang, which is in industrial use. A bytecode compiler for Urlang was then derived and proven correct, and a multiprocessor bytecode interpreter was implemented in Concert/C and proven correct. Finally it is argued that those features of Erlang which are not present in Urlang are easily added into our framework, either via source-to-source transformations into core Urlang or by means of straightforward additions to the operational semantics of CLAM.