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.

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.

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.

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.

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.