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.

Interactive proof assistants such as Agda have powerful applications in proving the correctness of software. Non-terminating programs, such as those containing infinite loops, result in execution paths of infinite length, which can introduce challenges when reasoning about such programs. Agda, as a total language, relies on the concept of coinduction for reasoning about potentially infinite structures. Mutiple methods for coinduction exist in Agda, each with difficulties related to usage or soundness. To evaluate these limitations, I implement traces and semantics for a simple imperative programming language, While, using Agda's various methods of coinduction. The different encodings are compared in their abilities and limitations, and from this I identify areas for improvement in Agda's coinduction support.

This thesis explores the formalization of Linear Temporal Logic (LTL) within the Agda proof assistant, focusing on the use of coinductive techniques to model infinite structures. Two primary questions guide this investigation: how can coinduction be employed to represent LTL formulas, and what are the limitations of Agda in doing so? To address these, the thesis presents two encodings of LTL: a deep embedding that models both syntax and semantics, and a shallow embedding that treats LTL propositions as infinite streams. Both approaches are evaluated by formalizing logical properties, deriving inference rules, and encoding the Towers of Hanoi as a temporal state system. The results demonstrate that coinductive techniques in Agda are expressive enough for reasoning about temporal logic, though challenges such as limited support for coinduction and usability issues remain. The findings provide insights into the strengths and limitations of Agda for modeling temporal logics and suggest directions for future work, including the exploration of sized types and extensions to first-order temporal logic.

Coinduction is used to model infinite data or cycles in Agda. However, it is not as well explored in Agda as induction. Therefore, support for it might be lacking compared to induction. I explore how this applies for the evaluation of lambda calculus, what the different encodings of lambda calculus using coinduction are, and how they compare to each other and to an inductive evaluator. The two models I looked at are modelling cycles in variable references and modelling cycles in recursive variables. Cycles in variable references can be modelled coinductively, however, they do not help with evaluation. Since the evaluator is not coinductive, it is not accepted by the termination checker, therefore, it is not safer than an inductive evaluator. Encoding recursion using coinduction does make the evaluator terminate, aiding in creating a correct evaluator. This comes with the downside of sacrificing clarity and ease of reasoning about the code.

Graphs are a widely used concept within computer science. Modelling graphs can be done in various ways, but the most popular approach is doing so inductively. When graphs contain cycles modelling them becomes less intuitive. A solution for this is using the dual of induction called coinduction, which has not been as well researched as induction. In this paper I explored the possibilities and limitations of coinduction in Agda by modelling graphs using coinduction. I looked at the struggles I encountered while coding in Agda. I also provide implementations of the graphs encodings. Suitability of the encodings is determined through experiments, in which properties about graphs are proven. Both guarded coinduction and musical coinduction were successful in all of the experiments. Creating an implementation using sized types was not successful. The main improvements I identified are concerning the ease of use for a new user of Agda. I recommend improving the documentation as well as the clarity of the error messages.

The proof assistant Agda supports coinduction, which can be used to reason about infinite and cyclic structures. The possibilities and limitations of using coinduction in Agda are not well known. To better understand these, I will implement Finite State Automata and their equivalence in Agda. Finite State Automata (FSA) is an example of a cyclic structure. FSA are an introductory model in computation theory, and can be used text processing and hardware design. Equivalence of two FSA is used in software and hardware verification. I created various encodings for FSA and prove equivalence between two deterministic FSA for each of them. At the end, I compared them and see whether they are limited by the support for coinduction in Agda.

Current tools for pattern matching computer programs often operate on abstract syntax trees or other static representations of programs. These approaches, though efficient, are fundamentally limited when it comes to capturing the dynamic behavior of programs. For example, it is not always possible to express (concise) syntactic patterns that capture programs which are semantically equivalent but differ in their syntactic representation. A tool that takes into account the behavior (or dynamic semantics) of programs would be able to capture programs that are semantically equivalent in a more concise manner with a single pattern. Additionally, taking into account program behavior leads to more precise pattern matching, by excluding unreachable paths of computation. In this thesis, we explore a novel method, based on behavioral models of programs, that allows patterns to take into account the dynamic semantics of a program. We propose the Dyno pattern language, in which concrete object language syntax can be used to express intuitive semantic patterns of programs. Pattern matching is performed by translating Dyno patterns to μ-calculus formulas and model checking these formulas against models extracted from object programs. Because our method is based on dynamic models of programs, we are fundamentally limited by the halting problem. In favor of precision, our method compromises on efficiency and termination guarantees. In particular, termination is not guaranteed when the extracted model of a program has infinitely many states. To recover termination in some cases, we provide the facility to express bounds on input parameters, limiting the search space while compromising on soundness. We recognize some limitations in our work, including a lack of match evidence (e.g. the location of a match in the object program’s syntax tree), as well as holes in Dyno’s expressiveness. To address the latter issue, we suggest operators that could be added to Dyno in the future.

Refactoring legacy systems is essential to maintain and modernize aging codebases, but traditional refactoring tools are often limited by language specificity and lack extensibility. This thesis introduces property-based Abstract Syntax Trees (ASTs), a flexible intermediate representation aimed at enhancing the language-parametric capabilities of refactoring tools. By leveraging Tree-Sitter, a parser generator that creates parsers that produce generic, property-based ASTs, this research adapts Renaissance, an existing industrial refactoring tool, to support multi-language extensibility with minimal additional effort. The adapted tool demonstrates equivalent functionality across C++, Java, and Python, maintaining features such as pattern matching, code rewriting, and placeholder handling. Experiments were performed, including experiments with exercises on an open-source repository, in order to highlight the practical benefits, extensibility, and limitations of this approach. This adaptation aims to showcase the feasibility of using property-based ASTs in enabling language-parametric tooling. This work lays the foundation for more centralized, cost-effective, and scalable tool development for industrial software refactoring.

WebDSL is a DSL for creating web applications, combining many different aspects and domains of web design in a single language. The dynamic semantics of this language are not defined, despite multiple attempts, abandoned due to complexity of the language and lack of expression of chosen frameworks. We adapt the algebraic effects and handlers approach and the framework introduced in Datatypes a la carte (Swierstra, 2008) to create a modular denotational semantics model of WebDSL, extending the framework by a bifunctor formulation for multi-sort syntax definition that allows us to distinguish between effects raised by different components of the language. In the process of defining the framework and semantics in Haskell, we encountered obstacles and of working with algebraic effects and handlers paradigm in the language, leading us to compile workarounds, solutions and pitfalls to avoid when constructing and maintaining such model. In evaluation of the framework approach with earlier attempts at defining dynamic semantics for WebDSL, we find algebraic effects and handlers to be a viable and successful approach for modelling a rich DSL such as WebDSL, and propose possible improvements to the WebDSL compiler.

This thesis investigates the potential of basing a program synthesis system on a de-
pendent type theory. This is an attractive research direction because it allows a very
flexible range of specification to be expressed within the same framework. We im-
plement a prototype of a search algorithm driven by unsolved constraints typically
generated during dependent type checking. We encode a range of synthesis prob-
lems from literature in our system, showcasing how it can be used for expressing
the specification and synthesizing programs that manipulate data. We empirically
establish the effect of constraint-directed aspect of our approach on performance,
based on the encoded problems.

The process of using formal verification, in order to ensure that a piece of software meets it functional requirements consists of three main steps: designing a model of the given piece of software, translating the functional requirements, which the piece of software must satisfy, into properties of said model and verifying that the model satisfies those properties. Traditionally, regardless of whether the piece of software is developed based on a predesigned model or the piece of software is developed first and its model is designed after that, the piece of software and its model are two separate entities. Therefore, aside from checking that the model satisfies its properties, it must also be verified that the model accurately represents the given piece of software. While this task may initially seem simple, it gets progressively more difficult, as the piece of software becomes more complex. And, if it turns out that the model is not accurate, then the entire formal verification process is invalid, since it does not provide any guarantees about the actual piece of software. In this thesis we present a solution to this problem: a way of modelling sequential effectful programs, such that the resulting models can be directly translated into runnable programs, thereby guaranteeing the models' accuracy. We achieve this by using algebraic effects, in order to model sequential effectful programs as instances of the coinductive free monad, that could then be translated into runnable pieces of software by applying the necessary effect handlers. Furthermore, we demonstrate that it is possible to express functional requirements as properties of such models using the first-order modal μ-calculus, a fixed-point dynamic logic which has previously been used to reason about labelled transition systems (e.g. in mCRL2).

This study explores the use of Code Churn and Pattern Size (PSIZ) metrics to identify bug-prone areas in Haskell codebases. The primary research questions addressed are whether these metrics can effectively predict areas of code instability and potential bugs. Our contributions include a comprehensive analysis of these metrics across three large Haskell projects, examining the correlation between high metric values and documented bugs. Our findings reveal that Code Churn is a significant indicator of potential bugs, with ’buggy’ files showing markedly higher mean code churn values. However, the PSIZ metric proved ineffective in predicting bug-prone areas, as the mean and median values for both projects and ’buggy’ files were similar and low. These results suggest that while Code Churn is a useful metric for identifying unstable code areas, PSIZ does not offer the same predictive value. Future research should expand the dataset and consider additional metrics to enhance the reliability of these findings.

The classification of bugs in functional languages is an understudied area, as opposed to imperative counterparts, such as Java. This paper acts as an initial step to cover this gap into two complementary directions. First, a dataset of 142 bugs from 10 Haskell FOSS repositories have been classified according to two taxonomies from literature in order to assess how well they handle the differences in programming paradigms. Based on our bug classifications, the first taxonomy has very little variance in types of bugs, with 86% of bugs being classified in the same category. On the other hand, the second taxonomy showed more potential as the bugs were more balanced between categories, but with occasional difficulties in classification, as some bugs fitted more than one type. Second, we performed interviews with four Haskell developers about their experience with bugs and the usefulness of these taxonomies in practice. They argued that while such taxonomies can prove useful, the context in which it is being used is more important. Thus, circumstances such as the size of the project and team, and stages of development need to be taken in consideration before trying to apply any taxonomy.

The Language Server Protocol (LSP) is a protocol that standardizes the way Integrated Development Environments (IDEs) and text editors communicate with language servers to provide language-specific features like autocompletion, go-to-definition, and diagnostics. While LSP has been widely adopted by mainstream programming languages, its adoption in dependently typed languages has been slower due to the unique challenges posed by their complex type systems and interactive theorem proving capabilities. This thesis explores the potential of LSP for enhancing the development of dependently typed programs, focusing on the Agda programming language. We present the implementation of a prototype LSP server for Agda that leverages scope checking to provide fast and responsive IDE features. We evaluate the performance of the prototype and compare its feature completeness with existing Agda development tools. Our findings demonstrate that scope checking can serve as a foundation for implementing efficient LSP features in Agda, offering a promising direction for improving the tooling and overall development experience for dependently typed languages.

The Correct-by-Construction (CbC) programming paradigm has gained increasing attention, particularly with the rise of dependently typed languages. The CbC approach is often characterized as rigid, rule-based construction process making it suitable for critical infrastructure like type-checkers, which are prone to bugs as they become more complex. However, the specific advantages and disadvantages of using the CbC approach for developing type-checkers in comparison to traditional programming languages remain unclear. Therefore, we investigate the development of a type-checker for a toy programming language extended with checked exceptions using the dependently typed programming language Agda. The results show that the CbC approach, combined with dependently typed languages, is highly effective for the very precise task of type-checker development. Despite the steep learning curve associated with these languages, this method offers notable benefits in ensuring the correctness and reliability of type-checkers. We conclude that this approach is a viable strategy for similar projects in the future.

Type-checkers are used to verify certain attributes of programs are correct. Avoiding bugs in type-checkers is especially important when accepting faulty programs has serious real-world consequences. Correct-by-construction programming aims to prevent such bugs by embedding proofs of a program's correctness within the program itself. However, this approach introduces different challenges, such as added complexity. Whether the benefits of correct-by-construction type-checkers outweigh these challenges for more complex language features remains uncertain. This paper investigates correct-by-construction type-checking for a toy language with polymorphic algebraic data types and pattern matching. We do this by implementing a type-checker in the dependently typed language Agda. We show that this approach guarantees a type-checker that does not accept ill-typed terms. Furthermore, we reflect on the challenges of this approach and argue that this approach should be used when a guarantee of correctness is required.

As programming languages become ever more sophisticated, there is growing interest in powerful and expressive type systems. Substructural type systems increase expressiveness by allowing the programmer to reason about the number of times and the order in which variables can be used. This can be used to model different kinds of memory allocation and to construct more expressive interfaces. However, implementing complex type systems requires complex type checkers – this complexity increases the chances of bugs in the type checker itself, which could lead to invalid programs being accepted or valid programs being rejected. The consequences of such bugs can range from programmer frustration to critical errors in production systems.

In this thesis, we develop a correct-by-construction type checker for a toy language with a substructural type system. We use Agda’s dependent type system to intrinsically ensure the soundness and completeness of the type checker. We discuss the advantages and disadvantages of the correct-by-construction approach and find that its complexity likely restricts it to specific use cases.

Various studies already exist about the lifecycle of software programs written in languages like Java, C and C++, but this is an under-reported area for the pure, functional programming language Haskell. This report explores steps in the development of Haskell programs, and particularly, of their bugs. By gaining more knowledge about a bug’s development and its different stages, possible patterns or trends can be found. Using these insights, developers could get a better understanding of the development process, and optimise it. The main question of the research is formulated as ‘What are the different stages of bugs in Haskell programs?’. We consider three different stages: bug introduction, bug detection and bug fixing. To gain more knowledge about these stages, different open-source Haskell repositories, and their bugs were analysed. We found the median time between the bug introduction and detection is 381 days. The median time between the bug detection and fixing turned out to be 3 days. Most bugs were detected and fixed at similar rates regardless of their complexity, except for bugs that were detected by the same developer who introduced the bug. In this case, the time it takes to detect the bug is 30% of the global median. These results motivate developers to check their code more extensively, as they detect bugs quicker than other developers would. It also motivates developers to work with shared code ownership, as having more developers familiar with the code should reduce bug-detection time. Moreover, this study shows that single-statement bugs, which needed a simple fix, occur 2.5 times more often in code when no test is written, which argues for developers to write more test code. Lastly, we recommend repository owners to be more strict with developers working structured and precisely so that they follow Git’s and the repository’s standards and write test code.

Haskell programming language has a long history of extensions which extend and
modify its syntax and semantics. They range from small quality-of-life syntax im-
provements, to complete overhauls of the type system. Such extensions are commonly
implemented directly as a part of Glasgow Haskell Compiler (GHC) or as plugins for
GHC through its plugin API. This paper looks at the present ecosystem of such lan-
guage extensions, identifying the key categories into which extensions can be separated,
based on how often and in which ways they are used, and their functionality.
We analysed which extensions are used in packages uploaded to Hackage, a central
open-source Haskell archive. We further extracted the metadata about the packages,
including the user-submitted tags and maintainer lists, to ascertain how and when are
language extensions used.
The result of our research is a combination of several proposed potential taxonomies,
that can be used by academics and practitioners alike.

Typecheckers help avoid bugs in code by catching errors early. Their implementation can, however, be incorrect, leading to inconsistencies in their operation. This research explores how we can use Agda and correct-by-construction programming to create a typechecker guaranteed to be correct in its implementation. For this purpose, I based a toy language on the simply typed lambda calculus extended with records and subtyping. The resulting typechecker is proven to be sound and complete with respect to the typing and subtyping rules of the toy language. This paper compares the correct-by-construction method to existing typecheckers. The new approach offers a greater degree of trust in its implementation but comes at the cost of being more demanding to develop and maintain.