Algebraic effects and handlers have become a popular abstraction for effectful computation, with implementations even in mainstream programming languages, such as OCaml. The operations of an algebraic effect define the syntax of the effect, while handlers define the semantics. This provides modularity, because we can choose which handler to apply to a computation. However, we cannot write handlers for many higher-order operations; operations that take effectful computations as parameters. Such higher-order operations can therefore not enjoy this modularity. Hefty algebras provide an additional layer of abstraction in the form of elaborations to make implementations of higher-order operations modular as well. Several languages, such as Koka, natively support algebraic effects and handlers. However, until now, no languages have been created with native support for higher-order effects. In this thesis, we introduce Elaine, a language featuring both handlers for algebraic effects and elaborations for higher-order effects. Additionally, we introduce implicit elaboration resolution; a type-directed procedure which infers the appropriate elaborations from context. We conjecture that hefty algebras are the semantics for Elaine. We provide a specification for Elaine, including its syntax definition, typing judgments and reduction semantics. This specification is implemented in a publicly available prototype which can type check and evaluate the set of example programs included with this thesis.

Effect handler oriented programming (EHOP) is a recently proposed programming paradigm, which aims to provide a separation of concerns by isolating the handling of side-effects from the main application logic. Nowadays, as the core concepts behind EHOP are being added to more and more programming languages, it is evident that EHOP is slowly but steadily growing in popularity. Therefore, it is important to explore the applicability of EHOP for different areas of software development. However, so far, very little research has been conducted on this topic and, thus, barely any possible application domains of EHOP have been investigated. This study focuses on a potential field of application of EHOP, which has not been covered by previous research, namely - text-based game development, and aims to determine the extent to which the usage of EHOP for text-based game development affects the modularity, readability and maintainability of the source code. This goal will be achieved by performing both a qualitative as well as a quantitative analysis of the source code of a text-based game, written in Koka - a state-of-the-art programming language, which supports EHOP. The results show that there are substantial benefits to using EHOP for text-based game development. It significantly improves the modularity, readability and maintainability of the source code at the cost of very little to no performance.

Effect Handler Oriented Programming is a promising new programming paradigm, delivering separation of of concerns with regards to side effects in an otherwise functional environment.
This paper discusses the applicability of this new paradigm to static code analysis programs.
Different code analyzers often have many similar, if not identical pieces of code which could be abstracted away.
This abstraction does not come natural to the programming paradigm of Functional Programming but are quite natural within EHOP.
The current programming languages do not yet seem up to the task of rapid generalization of code and elimination of duplicate pieces of code.
However, the concepts present in EHOP will almost certainly be able to eliminate much of this code reduction once the languages have matured further.
The implicit passing of functionality will also allow for clearer code with less unnecessary visual clutter.

Effect handler orient programming (EHOP) is a recently proposed programming paradigm that aims to provide a high-level abstraction in code. Using this paradigm, programmers are able to define operations as an effect, which are implemented by an effect handler. Functions can then use effects, allowing the effect operations to be used in this function. Depending on the effect handler that handles the effect, an effect can have different functionality. In this research, EHOP is compared to the traditional functional programming paradigm on readability, maintainability, modularity and performance for IO intensive applications. The comparison is carried out by two programming experiments that each apply one of the programming paradigms to create an HTTP server. The comparison of these programs show that EHOP improves the readability, maintainability and modularity but decreases the performance in response time and memory. The conclusion of this case study is therefore that EHOP affects IO intensive applications in a negative manner due to its performance overhead.

Grading and giving feedback to student submissions automatically is becoming more and more necessary with an increasing amount of students. To verify the correctness of student-written definitional interpreters, a program equivalence approach has been implemented, improved, and extended with new rules to make it more suited specifically for verifying interpreters. This approach is able to soundly recognise two different interpreters as equivalent. Interpreters can thus be compared to a correct interpreter to verify their correctness or be grouped with equivalent interpreters to be graded in batches. Using program equivalence in combination with other verification approaches can improve the process of giving feedback to students and help build up a collection of common errors made by students.

Definitional interpreters are difficult to test with a pre-defined test suite. This paper tries to determine the effectiveness of automatic testing of definitional interpreters, using concolic execution. First we develop a model for concolic execution of a functional language. Then we identify different categories of common mistakes when writing interpreters and test which are caught by concolic execution. We find that while concolic execution is promising, as it can find counterexamples for most errors in a small language, the model developed in this paper is not sufficient to generate counterexamples for more complicated languages.

Recent years have seen a surge of interest for dynamic testing techniques, one of which is symbolic execution. It is the main point of interest of this research paper, in which we give an overview of a framework for symbolically executing definitional interpreters. We will also discuss techniques that we made use of in developing the symbolic execution framework. The context of this project is the automated grading and validation of student submissions, and the results and performance of our approach will also be reviewed and criticized.