Software correctness is a hard problem. Dependently-typed programming languages like Agda help us to provide guarantees about software while writing it in a Correct-by-Construction (CbC) manner. However, the implementation of a dependently-typed programming language may contain bugs itself: Agda has bugs in its own implementation on a regular basis. Dependently typed-typed programming languages should therefore verify themselves in a Correct-by-Construction manner using their own components: self-verification. Agda Core aims to do this for Agda: it is a core language for Agda and provides a Correct-by-Construction type checker for itself derived from a trusted type theory, written in Agda.

Before Agda Core can be used as a true self-verifier for Agda and be integrated into Agda’s main compiler and type checker, more features from Agda need to be supported by it. In this thesis, we focus on Agda’s η-conversion for function types and record types. We formalize η-conversion for function types and record types with at least one field using untyped conversion: we also add support for records to Agda Core along the way. We also show progress towards a formalization of Agda’s η-conversion using typed conversion, which allows for formalizing the often tricky-considered η-conversion for Agda’s unit type. For all of these formalizations, we show that they can be added to Agda Core with reasonable effort. Overall, this work therefore provides an important step towards the ultimate goal of a self-verified type checker for Agda with support for all of Agda’s features, which decreases the future potential for bugs in Agda’s implementation with relation to η-conversion, and teaches us how to self-verify η-conversion for a dependently-typed language. ... Read more

Dependently typed languages and proof assistants such as Agda and Rocq improve the reliability of mathematical proofs and programs by representing logical propositions as types and proofs as programs inhabiting those types. Through the Curry--Howard correspondence, typechecking becomes proof checking, allowing correctness guarantees to be established by construction.

However, these guarantees ultimately rely on the correctness of the language implementation itself. Components such as typecheckers, conversion checkers, and termination checkers are typically implemented as algorithms whose correctness must be trusted independently from the theory they are intended to enforce.

Agda Core is a core language for Agda implemented in Agda itself, where language judgements are represented directly as dependent types and checking procedures become programs constructing evidence of those judgements. This thesis investigates how the same methodology can be applied to termination checking.

Termination checking is a fundamental component of dependently typed languages, since unrestricted recursion may compromise normalization and logical consistency. We explore how termination criteria can be represented as formal specifications together with executable proof-search procedures producing explicit certificates that the criteria hold.

We first study the guard condition, a structural recursion criterion based on descending recursive arguments, and implement a certified checker producing explicit evidence that the criterion holds. We then investigate the size change principle, a stronger termination criterion capable of handling a wider class of recursive and mutually recursive definitions. We formalize the corresponding rules in the same framework and discuss the challenges involved in constructing a fully executable checker for them.

More generally, this work explores the separation between declarative specifications of termination criteria and the algorithms used to search for certificates satisfying them. By expressing termination arguments directly in the type theory of the implementation language, the resulting infrastructure becomes simultaneously executable, inspectable, and partially verified.
... Read more

Testing constitutes an important part of software development for many engineers. Agda2Hs, a transpiler from Agda to Haskell, currently does not provide such testing functionality. Agda enables developers to express and formally verify properties directly within the source code, whereas Haskell benefits from an extensive ecosystem of tools and developers. By transpiling verified Agda code to Haskell, Agda2Hs offers the potential to combine the advantages of both languages. However, constructing formal proofs in Agda is challenging, as it requires the same creativity and insight needed for mathematical reasoning. Consequently, a proposition with a bug may be mistakenly seen as difficult to prove. Property-based testing can provide confidence in the correctness of a proposition before a proof is completed. This paper presents these testing functionalities in Agda2Hs by porting QuickCheck to Agda. Furthermore, correspondence proofs are introduced, which enable programmers to show formally that a test asserts the same property as a proposition. ... Read more

Property-based testing is a popular testing paradigm, especially common in the functional programming language Haskell through the QuickCheck library. On the other hand, Agda is a dependently-typed language used as a proof assistant and for software verification. Because of the need for software verification, Agda2hs was created as a tool for translating code between these two, combining proven functionality with practical execution.

This work explores making QuickCheck-compatible generators based on properties encoded in Agda. This should allow automating early checking of Agda proofs for correctness, as well as enabling conversion of formal specifications to executable tests for Haskell projects. A procedure is presented that permits creating advanced generators and checkers, and it is later evaluated in terms of multifaceted performance metrics. ... Read more

agda2hs is a compiler that allows compilation of dependently typed Agda language into readable Haskell modules. This has a benefit that a formal proof of correctness can be carried out on Agda side, and then used in more realistic context in Haskell. However, sometimes it might be beneficial to compile yet unproven functions to Haskell, to be able to use traditional testing methods to quickly discard incorrect implementations. In this paper, I explore the usefulness of using mutation testing in validating such property tests. I present modifications made to the existing Haskell MuCheck library to accommodate this workflow: a QuickCheck test adapter, an annotation mechanism that links tests to the functions they cover, and a way to mark already proven functions so they are not mutated. I evaluate the tool on several test cases, both written by hand and generated from Agda, including sorting algorithms and lambda calculus with De Bruijn indices. I find that the share of mutants equivalent to the original code varies greatly between functions, which makes the ratio of killed mutants hard to interpret on its own. The current implementation does not prove very practical at this stage, and I propose some improvements that could make this a useful tool for this particular workflow. ... Read more

Formally verified code written in dependently typed languages can be integrated into larger, non-verified code bases through source-to-source translation. The agda2hs compiler enables such integration by translating verified Agda code to readable Haskell, erasing proofs and type indices in the process. The properties that a program is verified against are encoded as such proofs and type indices, and are therefore also erased. Yet being able to check these properties is important: in the agda2hs workflow, verified code may depend on unverified Haskell libraries whose properties are assumed without proof and never tested.

In this paper, we present an extension to agda2hs that extracts postconditions and translates them into Haskell QuickCheck property tests. Since postconditions in Agda are encoded at the type level, they are not executable and cannot be translated to Haskell directly. We address this by deriving semi-decision procedures that check whether a proposition holds for given inputs. We cover postconditions expressed as separate lemmas, sigma types, and indexed datatypes. We implement lemma-to-test translation as a working agda2hs extension; it requires the user to write the decision procedure by hand. We present the automatic derivation of such procedures as an algorithm design with worked examples. ... Read more

This research aims to explore using property based testing to find counterexamples for proving statements about programs in Agda2hs. I have created an extension to Agda2hs to translate type class laws into QuickCheck properties and evaluated on real-world Haskell code to evaluate its effectiveness. I found that having relatively cheap to run tests compared to formalizing helped save time ensuring definitions were correct before formalizing statements. ... Read more

Program synthesis is a computationally difficult task. Budgeted search seems to be a relatively unexplored method of performing program synthesis tasks. This paper describes a budgeted program synthesis implementation that makes use of subprograms it discovers during attempts and leverages them in future attempts in hopes of finding an optimal solution faster. The approach performed slightly worse than most of the control synthesis task runs during experiments. However, some specific cases were discovered for which the budgeted synthesis ran faster than the control synthesis task. ... Read more

Program synthesis automatically generates pro-grams satisfying given specifications through sys-tematic search over candidate programs. This pa-per explores an enhancement to Herb.jl, a pro-gram synthesis framework, by implementing a two-phase approach that alternates between a ”wak-ing” phase that generates candidate programs, anda ”sleeping” phase that identifies frequently occur-ring subprograms and refactors the grammar ac-cordingly. The sleeping phase uses Clingo to dis-cover common patterns, which are incorporatedinto the grammar to enable more efficient synthesis.I investigate whether this iterative refactoring ac-celerates synthesis, and identify types of problemswhere it provides improvements. This work con-tributes to understanding how grammar compres-sion and abstraction discovery can enhance pro-gram synthesis efficiency.

https://github.com/jelleromer/herb-bep ... Read more

Dependently typed languages allow developers to enforce compile time correctness of programs via the type system. These guarantees however, have to be proven with code, incurring a runtime and memory overhead. These costs can be avoided by using erasure (based on Quantitative Type Theory (QTT)) to omit code marked as erased (e.g. the aforementioned guarantees), which enables a separation between compile-time and run-time concerns.
Erasure annotations can give rise to types that are nominally different but structurally equal at runtime. We name functions between these types that behave like the identity at runtime, runtime identity (runid) functions. Current solutions do not have a structured way to reason about these runid functions as a first class member of the type system. This means programmers have no way to enforce that the compiler will erase these functions nor use the information of runid status to propagate optimizations, like defining runid functions that are polymorphic on some underlying runid function.
This thesis introduces a lightweight core language that extends a QTT-style, intensional Martin-Löf Type Theory (MLTT) with explicit markers for runid functions. We extend the type system with a static check that ensures runid-marked functions are equivalent to the identity function at run-time, using a novel run-time equivalence relation.
As a secondary contribution, we define a semantics for our language inspired by Normalization by Evaluation (NbE). Our semantic domain is extensional, i.e. function equality is extensional, and agnostic to the compilation target, providing a clean model for reasoning about erased and runtime identity behaviour. We prove the soundness of our static analysis by showing that runid-equivalent terms are mapped to equal semantic values ... Read more

Memory access bugs exist in almost every compiled programming language. To solve this, modern programming languages like Rust use complex variable ownership systems that ensure memory safety. These kinds of ownership systems can be used to distinguish between variables that can only be read and ones that can be safely written to as well. These strict ownership rules are, however, limited when using external libraries. While the Foreign Function Interfaces (FFI) used to show what arguments external functions use can be written with these ownership requirements, enforcing them on the side of the external library is not required, potentially resulting in a discrepancy between what is expected on Rust's side and what happens in the external library.

To solve this problem we propose a novel mechanism for detecting memory safety violations across language boundaries. We implemented it in a tool called MiriPBT: a combination of MIRI, a tool that can enforce ownership rules at runtime, MiriLLI, an extension of MIRI that allows ownership rules to be enforced on the other side of the FFI boundary, and Property Based Testing, which allows us to greatly increase the size of the domain we can test. We use Rust's type system to generate inputs for the PBT and use the runtime checks of MIRI and MiriLLI to check if any ownership rules are violated. Finally we present the result of the PBT in a format an average Rust user can easily understand, helping them resolve any FFI related ownership bugs in their code. ... Read more

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

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

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

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

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

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

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

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

The Statix meta-language is a domain-specific language that is used to describe specifications for type systems using high-level declarative inference rules. Type checkers
can be automatically generated from these rules, saving one from the burden of writing
it manually. One of the problems with these generated type checkers is performance;
handwritten type checkers usually outperform the generated ones. Statix uses the formalism of scope graphs to represent name binding, and querying these scope graphs is
known to be the main performance bottleneck. Improving the performance of queries
means improving the performance of the type checkers generated by Statix.

In this thesis, we propose a memoised variant of the current state-of-the-art query
resolution algorithm that memoises data encountered during graph traversal, reducing
future queries to a cache lookup. We also identify common patterns in real-world scope
graphs and link those to the name binding structure that created them. We construct a
synthetic dataset with these patterns that is used to evaluate query resolution algorithms
with microbenchmarks. This gives us more granular information on what name binding
structures benefit most, if at all, from memoisation.

The results of these benchmarks are the performance differences between the memoised algorithm and the current state-of-the-art algorithm per identified pattern. They
show that our proposed algorithm breaks even in terms of performance after only two
queries for most patterns. Furthermore, we demonstrate that our proposed algorithm
and the current state-of-the-art provide identical efficacy. The tradeoffs are twofold: the
cache increases the memory usage of query resolution significantly and the query resolution parameters were tweaked to make caching possible, but less versatile. The changed
query parameters’ limitations should only be theoretical however, the Statix specification
for Java 1.5 has 23 out of 25 fully compatible queries. ... Read more