An increasingly popular application of parallel computing is Big Data, which concerns the storage and analysis of very large datasets. Many of the prominent Big Data frameworks are written in Java or JVM-based languages. However, as a base language for Big Data systems, Java still lacks a number of important capabilities such as processing very large datasets and distributing the computation over multiple machines. The introduction of Streams in Java 8 has provided a useful programming model for data-parallel computing, but it is limited to a single JVM and still does not address Big Data issues. This thesis contends that though the Java 8 Stream framework is inadequate to support the development of Big Data applications, it is possible to extend the framework to achieve performance comparable to or exceeding those of popular Big Data frameworks. It first reviews a number of Big Data programming models and gives an overview of the Java 8 Stream API. It then proposes a set of extensions to allow Java 8 Streams to be used in Big Data systems. It also shows how the extended API can be used to implement a range of standard Big Data paradigms. Finally, it compares the performance of such programs with that of Hadoop and Spark. Despite being a proof-of-concept implementation, experimental results indicate that it is a lightweight and efficient framework, comparable in performance to Hadoop and Spark.

This thesis introduces a new object-based language FlexibO to support prototype development paradigm and more importantly, program static analysis. FlexibO offers extreme flexibility and hence enables developers to write programs that contain rich information for further analysis and optimization. FlexibO interpreter's seamless integration with Java (including direct access to Java classes and methods and direct inheritance of Java classes) makes it a suitable tool for fast prototype software development. FlexibO's extreme flexibility allows developers to redefine the behavior of program evaluation by overriding its default evaluation method. This mechanism can be used to translate FlexibO to other efficient languages. In this thesis we design a translator in FlexibO to translate Bulk-Synchronous Parallel specifications (expressed in FlexibO) to executable C pro grams linked with BSPLib. Before translation, the tool first checks syntax and type, then statically analyzes potential communication conflicts, and finally generates C code. The translation process can accurately analyze primitive commands but require approximation (using abstract interpretation) for more advanced commands such as loops. The appropriateness of the translator and the associated static analysis can be formally analyzed using the technique of normal form.

This work treats word problems of finitely generated groups and variations thereof, such as word problems of pairs of groups and irreducible word problems of groups. These problems can be seen as formal languages on the generators of the group and as such they can be members of certain well-known language classes, such as the class of regular, one-counter, context-free, recursively enumerable or recursive languages, or less well known ones such as the class of terminal Petri net languages. We investigate what effect the class of these various problems has on the algebraic structure of the relevant group or groups. We first generalize some results on pairs of groups, which were previously proven for context-free pairs of groups only. We then proceed to look at irreducible word problems, where our main contribution is the fact that a group for which all irreducible word problems are recursively enumerable must necessarily have solvable word problem. We then investigate groups for which membership of the irreducible word problem in the class of recursively enumerable languages is not independent of generating set. Lastly, we prove that groups whose word problem is a terminal Petri net language are exactly the virtually abelian groups.

Type error reports provide programmers with a description of type errors which exist in their code. Such descriptions are frequently of poor quality, as they often present just one point in the program, rather than all locations in the code which contribute to that type error. Skalpel is a type error report system for the Standard ML language which tackles this problem, by presenting all and only the locations in the program which contribute to the type error. While the original Skalpel gives substantially better error reports than comparable systems, it has a number of limitations such as a lack of support for language features and poor efficiency. In this research we have made a number of contributions, including a full critique of both the Skalpel core theoretical system and its extensions, support for the remaining features of Standard ML, an analysis and improvements to the efficiency, and an investigation for the first time on Skalpel’s theoretical properties.

Conventional parallel programming is complex and error prone. To improve programmer productivity, we need to raise the level of abstraction with a higher-level programming model that hides many parallel coordination aspects. Evaluation strategies use non-strictness to separate the coordination and computation aspects of a Glasgow parallel Haskell (GpH) program. This allows the specification of high level parallel programs, eliminating the low-level complexity of synchronisation and communication associated with parallel programming. This thesis employs a data-structure-driven approach for parallelism derived through generic parallel traversal and evaluation of sub-components of data structures. We focus on evaluation strategies over list, tree and graph data structures, allowing re-use across applications with minimal changes to the sequential algorithm. In particular, we develop novel evaluation strategies for tree data structures, using core functional programming techniques for coordination control, achieving more flexible parallelism. We use non-strictness to control parallelism more flexibly. We apply the notion of fuel as a resource that dictates parallelism generation, in particular, the bi-directional flow of fuel, implemented using a circular program definition, in a tree structure as a novel way of controlling parallel evaluation. This is the first use of circular programming in evaluation strategies and is complemented by a lazy function for bounding the size of sub-trees. We extend these control mechanisms to graph structures and demonstrate performance improvements on several parallel graph traversals. We combine circularity for control for improved performance of strategies with circularity for computation using circular data structures. In particular, we develop a hybrid traversal strategy for graphs, exploiting breadth-first order for exposing parallelism initially, and then proceeding with a depth-first order to minimise overhead associated with a full parallel breadth-first traversal. The efficiency of the tree strategies is evaluated on a benchmark program, and two non-trivial case studies: a Barnes-Hut algorithm for the n-body problem and sparse matrix multiplication, both using quad-trees. We also evaluate a graph search algorithm implemented using the various traversal strategies. We demonstrate improved performance on a server-class multicore machine with up to 48 cores, with the advanced fuel splitting mechanisms proving to be more flexible in throttling parallelism. To guide the behaviour of the strategies, we develop heuristics-based parameter selection to select their specific control parameters.

The design and implementation of critical controllers benefit from development in a formal method such as B. However, B does not support execution specification directly, which is a requirement in controller design. The aim here is to develop a set of annotations so that they can be used by a B design engineer to capture execution requirements, while creating the B model. The annotations, once shown to be machine-annotation consistent with the B machine, can be used independently from the machine to assess the correctness of CSP controllers developed to detail the control behaviour. CSP-B is a formal method integration that can be used to develop critical controller with both state and event behaviour. The advantages of using annotations is that the execution requirements can be captured and shown to be machine-annotation consistent during state operation development, and that a control loop invariant does not have to be independently developed. Handel-C is used on route to hardware synthesis as it supports the implementation of concurrency and the manipulation of state. Annotations are utilised again to guide the translation of the B and control annotations into Handel-C. This PhD. work has three main aims. Firstly, to introduce a set of annotations to describe control directives to permit controller development in B. The annotations capture execution requirements. They give rise to proof obligations that when discharged prove that the annotations are machine-annotation consistent with the machine they are written in, and therefore will not cause the machine to diverge. Secondly, we have proven that CSP controllers that are consistent with the annotations will preserve the non-divergence property established between the machine and the annotations. Thirdly, we show how annotation refinement is possible, and show a range of mappings from the annotated B and the consistent controller to Handel-C. The development of mappings demonstrates the feasibility of automatic translation of annotated B to Handel-C.

The recent popularity of Field Programmable Gate Array (FPGA) technology has made the synthesis of Hardware Description Language (HDL) programs into FPGAs a very attractive topic for research. In particular, the correctness in the synthesis of an FPGA programming file from a source HDL program has gained significant relevance in the context of safety or mission-critical systems. The results presented here are part of a research project aiming at producing a verified compiler for the Handel-C language. Handel-C is a high level HDL based on the syntax of the C language extended with constructs to deal with parallel behaviour and process communications based on CSP. Given the complexity of designing a provably correct compiler for a language like Handel-C, we have adopted the algebraic approach to compilation as it oers an elegant solution to this problem. The idea behind algebraic compilation is to create a sound reasoning framework in which the a formal model of the source Handel-C program can be embedded and refined into a formal abstraction of the target hardware. As the algebraic rules used to compile the program are proven to preserve the semantics, the correctness of the entire compilation process (i.e., semantic equivalence between source and target programs) can be argued by construction, considering each programming construct in isolation, rather than trying to assert the correctness of the compilation in a single step. Regarding hardware synthesis, the algebraic approach has already been applied to subsets of Occam and Verilog. Our work builds on some ideas from these works but focuses on the more complex timing model imposed by Handel-C. Moreover, our work covers features like shared variables, multi-way communications and priorities which, to our knowledge, have never been addressed within the framework of algebraic compilation. Finally, one characteristic of the algebraic approach is that the basic reduction laws in the reasoning framework are postulated as axioms. As an invalid axiom would allow us to prove invalid results (up to the extent of being able to prove a false theorem) we are also concerned about the consistency of the basic postulates in our theory. We addressed this by providing denotational semantics for Handel-C and its reasoning extensions in the context of the Unifying Theories of Programming (UTP). Our UTP denotational semantics not only provided a model for our theory (hence, proving its consistency) but also allowed us to prove all the axioms in the compilation framework.

Meta-evolution, the ability to generate novel ways of generating novelty, is one of the major goals of Artificial Life research. Biological systems can be seen to perform open-ended meta-evolution, but unfortunately this has proved very difficult to replicate within computer programs. This thesis defines a theoretical framework for thinking about the issues in this area and charting out possible solutions. We use this framework to take some tentative steps towards meta-evolutionary algorithms. We begin with a review of how meta-evolution has developed historically, through different novelty-generation algorithms. We describe previous algorithms in terms of their biological model and their computational model, to distinguish their biological inspiration from their computational implementation details. We conclude that the route to meta-evolution lies in enriching the biological models of current algorithms, rather than their computational ones. We use the theoretical idea of embodiment to analyse both biological and computational systems, and decompose the problem of achieving meta-evolution. We present a new definition of embodiment, allowing the concept to be applied to biological systems. We conclude that biological systems achieve meta-evolution by their embodiment within the physical world. We notice that current computational systems have poor embodiment within their virtual worlds. This leads to the hypothesis that improving the embodiment of computational systems, within virtual worlds, is a route to improving their meta-evolution. In discussing how embodiment can be realised in virtual worlds, we use Artificial Chemistries as a language in which to program embodiment. We present a new definition of Artificial Chemistries, mapping their components onto our definition of embodiment. We end by presenting a new Artificial Chemistry, GraphMol, designed with embodiment in mind. We use GraphMol to embody the process of copying a string, and analyse its meta-evolution via a range of different experiments.

The graph programming language GP (Graph Programs) 2 and its implementation is the subject of this thesis. The language allows programmers to write visual graph programs at a high level of abstraction, bringing the task of solving graph-based problems to an environment in which the user feels comfortable and secure. Implementing graph programs presents two main challenges. The first challenge is translating programs from a high-level source code representation to executable code, which involves bridging the gap from a non-deterministic program to deterministic machine code. The second challenge is overcoming the theoretically impractical complexity of applying graph transformation rules, the basic computation step of a graph program. The work presented in this thesis addresses both of these challenges. We tackle the first challenge by implementing a compiler that translates GP 2 graph programs directly to C code. Implementation strategies concerning the storage and access of internal data structures are empirically compared to determine the most efficient approach for executing practical graph programs. The second challenge is met by extending the double-pushout approach to graph transformation with root nodes to support fast execution of graph transformation rules by restricting the search to the local neighbourhood of the root nodes in the host graph. We add this theoretical construct to the GP 2 language in order to support rooted graph transformation rules, and we identify a class of rooted rules that are applicable in constant time on certain classes of graphs. Finally, we combine theory and practice by writing rooted graph programs to solve two common graph algorithms, and demonstrate that their execution times are capable of matching the execution times of tailored C solutions.

Identifier names are the principal means of recording and communicating ideas in source code and are a significant source of information for software developers and maintainers, and the tools that support their work. This research aims to increase understanding of identifier name content types - words, abbreviations, etc. - and phrasal structures - noun phrases, verb phrases, etc. - by improving techniques for the analysis of identifier names. The techniques and knowledge acquired can be applied to improve program comprehension tools that support internal code quality, concept location, traceability and model extraction. Previous detailed investigations of identifier names have focused on method names, and the content and structure of Java class and reference (field, parameter, and variable) names are less well understood. I developed improved algorithms to tokenise names, and trained part-of-speech tagger models on identifier names to support the analysis of class and reference names in a corpus of 60 open source Java projects. I confirm that developers structure the majority of names according to identifier naming conventions, and use phrasal structures reported in the literature. I also show that developers use a wider variety of content types and phrasal structures than previously understood. Unusually structured class names are largely project-specific naming conventions, but could indicate design issues. Analysis of phrasal reference names showed that developers most often use the phrasal structures described in the literature and used to support the extraction of information from names, but also choose unexpected phrasal structures, and complex, multi-phrasal, names. Using Nominal - software I created to evaluate adherence to naming conventions - I found developers tend to follow naming conventions, but that adherence to published conventions varies between projects because developers also establish new conventions for the use of typography, content types and phrasal structure to support their work: particularly to distinguish the roles of Java field names.