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.

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.

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.

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.

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.

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.

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.

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.

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.