Debugging is a fundamental part of software development, yet adding debugger support to new programming languages remains a complex and underexplored challenge. This report presents the design and implementation of source-level debugging for Hylo, a new systems programming language that emphasises generic programming and mutable value semantics. To achieve this, we extend the Hylo compiler to emit DWARF debug information, enabling seamless integration with the LLDB debugger. Our approach is incremental and guided by the behaviour of the Clang C++ compiler, allowing us to support Hylo core language features, such as variables, functions, user-defined types, and generics. We also identify and analyse key limitations, including challenges in representing Hylo's fine-grained variable lifetimes and projections, enabling evaluation of complex expressions in LLDB, and supporting Hylo's dynamic types (i.e., existentials). Beyond Hylo, this work aims to outline a general, reusable methodology for equipping new programming languages with modern debugging capabilities, improving their usability and adoption.

Proof assistants are tools that allow programmers to write formal proofs. However, despite the improvements made in recent years, there is still a limited number of published user studies in improving the usability of dependently-typed proof assistants. This is especially true for investigating the effects of enhancing error messages on novice programmers, even though it is a popular topic for imperative languages.

This thesis aimed to help fill this gap in knowledge by using Agda as a research vector. We implemented hint enhancements for the error messages displayed upon three common mistakes: forgetting whitespace, using confusable Unicode characters, and supplying too few arguments to a function. A between-participants user study was then conducted with 70 students to determine the effects that these error messages had on the usability of Agda.

Results showed statistically significant improvements in the number of compiling submissions, and the rated "helpfulness" of the error messages (when compared to the original messages without hints). However, we were not able to determine if there was any statistically significant impact on the overall speed at which students resolved the errors. Furthermore, while we identified decreases in the ratings of "incorrect" hints, they did not appear to significantly influence the success rate, or time taken to fix an error. We concluded that enhancing error messages with hints is a promising avenue for improving the usability of dependently-typed proof assistants.

Interoperability with C is critical for new systems languages, yet achieving a high-fidelity bridge requires navigating a complex space of trade-offs between usability, portability, and maintainability. Beyond mastering platform-specific ABIs and C dialects, a robust tool must decipher C's "semantic dialects"—programming conventions where syntax alone is insufficient to determine intent, such as an enum representing a set of mutually exclusive cases, a collection of combinable bitflags, or simply a group of named integer constants. These idioms defy rigid, one-size-fits-all translation.

This paper presents a principled technical design for a C interoperability layer for Hylo that addresses these challenges. We propose an architecture that leverages Clang for high-fidelity parsing and correct ABI handling, and a semantic mapping framework based on sensible defaults with developer-driven customization. This approach allows ambiguous C constructs to be mapped to the most appropriate and idiomatic Hylo representation, balancing automation with developer control. The result is a complete roadmap for a powerful and usable interoperability solution.

Addressing the challenge of reasoning about programs across different evaluation strategies has long been a concern in functional programming. Levy's introduction of the call-by-push-value (CBPV) calculus represents a significant step forward in tackling this. His paradigm provided a more powerful approach that can encapsulate both call-by-value and call-by-name that was even later extended to include call-by-need. In this paper we present the development of an interface that integrates the theory of CBPV with algebraic effects and handlers. We demonstrate how this technique enables the definition and execution of programs, highlighting its capability to defer computations across different evaluation strategies and define operations in a modular fashion. We then define and prove a set of laws that can be used with our interface to reason about programs under varying evaluation regimes. This approach not only enhances the flexibility and modularity of language and library implementation but also allows for direct reasoning about these implementations, beyond the meta-level abstraction.

Algebraic effects and handlers are a new paradigm in functional programming. They aim at modularly handling side effects, by separating the declaration of those effects, from how they are handled. In this paper, we show how we can leverage their use to create an interface for concurrency using algebraic effects for which we can prove a list of concurrency laws, and also design handlers that allow us to run programs concurrently, thereby demonstrating the practical application of algebraic effects and handlers in managing concurrency.

Algebraic effects and handlers are a new programming technique that allows for the definition of abstractions as interfaces, with handlers providing modular, concrete implementations of these interfaces. In this paper, we consider algebraic effects and handlers implemented in Haskell, and explore how they behave under fixed-point (value) recursion. We give different possible implementations of fixed-point combinators for effectful functions, and work out their evaluation processes. We find that these functions behave very predictably under normal fixed-point recursion, while value recursion seems to be a much harder problem. We discuss the difficulties of implementing value recursion, and several possibile solutions are explored, but the question of whether a fixed-point combinator with value recursion semantics can exist at all in the presence of algebraic effects remains unanswered.

When writing functional code that composes multiple recursive functions that operate on a datastrcuture, we often incur a lot of computational overhead allocating memory, only to later read, use, and discard this information.
This can be alleviated using fusion, a technique that combines these multiple recursive datastructure traversals into one.
This thesis explores shortcut fusion using (Co)Church encodings based on the work of Harper (2011), focusing on two questions: What is needed to reliably achieve fusion in Haskell, and the correctness of these transformations through a formalization in Agda.

The first contribution replicates and extends Harper's (Co)Church encodings in Haskell, uncovering optimizer weaknesses and providing practical insights for achieving fusion within Haskell.
The second contribution formalizes these encodings in Agda, leveraging parametricity and the category theory described by Harper.
The formalization proves the equivalence of these encoded functions to the unencoded ones, showing that the encodings are in fact isomorphisms, as long as parametricity (Wadler, 1989) is assumed.

These findings highlight the effectiveness and correctness of shortcut fusion techniques and show the promise of shortcut fusion: Reduce the computational overhead associated with functional programming while retaining its nice, compositional properties.

Algebraic effects and handlers has been a popular approach for modelling side-effects in functional programming languages. Focusing on composability and modularity, this approach separates the effectful syntax from its semantics, which helps programmers to create effect abstractions such that their implementation can be modified without changing the syntax. However, there exist mainstream functional programming languages, like Haskell, which lack built-in frameworks to accommodate specifying side-effects in this manner. In this paper, we provide an interface for Haskell's Software Transactional Memory (STM), a concurrency abstraction, in the framework of algebraic effects and handlers from prior literature. We embed our implementation into a simple concurrency model using higher-order effects, in order to demonstrate it is possible to define and execute effectful concurrent programs that obey the semantics of Haskell's STM. Furthermore, we prove that our implementation satisfies the necessary laws governing our interface, such that programmers can easily reason about programs using our STM model.

Effect handler oriented programming or EHOP for short, is a new programming paradigm aiming to achieve separation of concerns in code which will lead to modular, readable and maintainable code. Since EHOP is significantly new, it is important to assess and compare it against traditional, commonly used paradigms in order to see if a wider adoption of EHOP would prove beneficial to computer science. In this research, EHOP was compared with traditional paradigms under the context of data processing applications. An Excel-like command line application called “MiniExcel” was implemented from scratch. Moreover, “Hierarchical EHOP”, a new structural pattern for EHOP was defined which enforces rules between concepts and produces a readable code structure. The main conclusions of this research can be summarized by the following statements. EHOP produces more modular, readable and maintainable code compared to traditional paradigms. Implementing additional concepts and updates to code is seamless using EHOP, yet the lack of development in EHOP’s ecosystem raises frustrating errors and requires the developer to implement libraries that are usually built-in for languages that support traditional paradigms. Functional programming produces faster running code, but EHOP is more memory efficient. Therefore, for applications that interact with users EHOP is the better choice and for applications that only execute code functional programming is more suitable.

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