An Executable Rewriting Logic Semantics for Concurrent Haskell

Abstract

Concurrent Haskell is an extension to the pure-functional language Haskell that provides primitives to construct concurrent programs. There is already an operational semantics for this extension as well as a huge number of semantics for the core language in a variety of different styles. The aim of this thesis is to present a coherent dynamic semantics of Concurrent Haskell comprising a wide range of its features including laziness, pattern matching, mutual recursion, imprecise exceptions (synchronous and asynchronous), I/O and of course concurrency. This is done using Meseguer\textquoterights semantic framework of rewriting logic. Despite the algebraic formulation the style of the semantics is still operational. Moreover the resulting rewrite theory of the semantics of Concurrent Haskell is shown to meet certain requirements that makes it executable by the Maude system, an implementation of rewriting logic. This and the modularity and extensibility of the developed rewrite theory distinguishes it from previous semantic definitions for Haskell in general and makes it furthermore usefull for practical purposes. In addition the choice of the formulation of the semantic rewrite theory is justified by showing its equivalence to several existing semantics each of which only covers a different subset of the language features that are considered here.

Categories: Rewriting, Formal Verification, Functional Programming