[L2] ================================================ AMAST Links 02 01

             Compiler Correctness for Concurrent Languages
                  Dave Gladstein (daveg@ccs.neu.edu)

  My PhD thesis is available online, via my _WWW page_ at
URL: http://www.ccs.neu.edu/home/daveg/
or via _anonymous ftp_ at
URL: ftp://ftp.ccs.neu.edu/pub/people/daveg/thesis.ps.Z

  *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.