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

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

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

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

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

Formally verified programs can be embedded in larger non-verified code bases by means of syntactically faithful source-to-source translation: systems like Agda2Hs make it possible to translate verified code written in a dependently typed programming language to a general-purpose functional programming language, Agda and Haskell in this case. Such systems can enable verification for critical functionality while keeping wider ecosystem access and easier to write code for peripheral functionality. However, this interfacing leaves a gap in the formal guarantees of the verified code: preconditions that were only expressible as a dependent type and have thus got erased upon translation might not be met. We present runtime checking these preconditions as a way to close this gap and ensure that computation does not continue on ill-formed input. As an extension to Agda2Hs, we have implemented a solution to automatically insert runtime checks for the preconditions and only make those definitions accessible in the output that are also checkable. The runtime check insertions do not only cover functions, but also data types and non-class records in the form of smart constructors; higher-order erased arguments are supported as well. We make a formal completeness analysis of a simplified version of the checks we generate for well- and ill-typed programs.
In our solution, class instances are not supported for runtime checking due to their different nature, and capabilities for recovering from a failed runtime check are still rudimentary. Despite these limitations, we conclude that a closure of the input precondition verification gap is possible, and that the development time trade-off in comparison to handwriting checks can be worthwhile. ... Read more

Agda is a language used to write computer-verified proofs. It has a module system that provides namespacing, module parameters and module aliases. These parameters and aliases can be used to write shorter and cleaner proofs. However, the current implementation of the module system has several problems, such as an exponential desugaring of module aliases. This thesis shows how the module system can be changed to address these problems. We have found that we do not need any desugarings during type-checking, but can instead handle module parameters and aliases during signature lookup by making a small change to the scope-checker, completely eliminating any exponential growth problems and unnecessary complexity. This will allow users to make more effective use of the module system, simplifying their proofs. Furthermore, the improvements to the module system will allow future research to fix the problems with Agda's implementation of pretty-printing, records and open public statements. ... Read more

Data types and pattern matching are fundamental concepts in programming. Data types define the structure of data, while pattern matching allows efficient manipulation and extraction of the same data. This text provides an overview of different implementation techniques for type systems regarding data types and pattern matching in the existing literature. Data types considered include inductive, coinductive, and mutually inductive, while the main pattern-matching methods considered are decision trees, backtracking finite state automata, and term decomposition. Though approaches for implementation techniques of data types can be compared more objectively, separate approaches for pattern matching have different benefits and drawbacks, thus, a one-fits-all technique does not exist. ... Read more

Names are essential for structuring and reason-ing about programs. However, the implementation of names differs across many programming lan-guages. There is an bundance of choice between various implementation techniques with regards to name-binding techniques. As such, when design-ing a programming language it is not clear which technique one should choose. This paper attempts to give an exhaustive overview of the various tech-niques that exist, compares them on properties such as alpha-equivalence, ease of implementation and enforcing well-scopedness. Furthermore, the pos-sibility of a one-fits-all solution is explored. ... Read more

Type checkers are invaluable tools which help programmers write correct programs. Fast and efficient type checkers are required to enable adoption of such tools in practice.

This study aims to provide an explorative overview of proposed efficiency improvements for type checkers. This provides language implementers insight in what approaches exist to increase the performance of their type checker.

Efficiency improvements are divided into three general approaches: incrementalization, parallelization, and algorithmic improvements. For each category, we discuss the implementation techniques and performance for several proposed approaches.

This study finds that a wide variety of approaches exist to increase the efficiency of type checkers. Based on reported benchmark results, incrementalization and parallelization are promising approaches to writing fast type checkers. ... Read more

The success of dynamically typed languages such as Python has resulted in an increased interest in supporting type inference in statically typed lan- guages. Type inference refers to automatic type detection based on surrounding context and allows retaining the type safety (and other advantages) of static types, while matching the ease of use of dy- namically typed languages. Unfortunately, imple- menting type inference can be tricky. Researchers have been proposing various methods for type in- ference ever since the 1970s, however there is no single solution that works for all languages. This paper presents and analyses the proposed methods together with motivations, intuitions, use-cases and examples from practice with the aim of helping new programming language developers understand type inference principles and choose the right technique for their needs. ... Read more

While dependent types can allow programmers to verify properties of their programs, implementing a type checker for a dependent type theory is often difficult. This is due to the fact that, in the presence of dependent types, deciding the equality of types - conversion checking - becomes non-trivial. Due to an identified gap in literature regarding a survey of existing techniques for implementing conversion checking in the presence of dependent types, this paper aims to provide an exploratory overview of the current state of this field.

We identify five distinct implementation strategies within this paper. Four of these techniques were different from a theoretical standpoint - \nameref{naive}, \nameref{NbE}, \nameref{generalShape}, \nameref{hersub}, and a technique using congruence closure. They all have different benefits and drawbacks regarding their portability, extendability to richer type systems, efficiency, and decidability. Additionally, three techniques that focused on improving the efficiency of conversion checking through the use of an abstract machine or compilation into native code were found. ... Read more

In this thesis, we develop a new library for Agda named Attic, which allows us to create and compose proof tactics that can be used to generate terms through reflection. Such tactics can be converted to Agda macros, allowing them to be used in term positions where they can generate term solutions of the expected type. Tactics can make the development of proofs faster by making proofs easier to read and write.

This project can be seen as a sister project to Ataca, which is an earlier attempt at developing tactics that operate through reflection. Attic explores new mechanisms of operation, such as non-determinism with iterators to allow for multiple solutions, and the use of deferred unification, so that the final proof term is only fully constructed at the end of tactic evaluation.

To allow for the representation of both finite and infinite sequences that can be consumed step-by-step, we have implemented the iterator data type in Agda. Although iterators existed in other systems previously, an Agda implementation had not been made. These iterators underpin the branching mechanism in tactic instructions, and support operations that can be used to generate, transform and filter values.

Finally, we have implemented a number of tactics and operations that are commonly found in other proof assistants. We also compare the resulting library to the Ataca library and examine the differences in runtime for a small test case. While Attic is not yet a complete solution, we present new ideas that may be incorporated in future tactic systems. ... Read more