Improving Agda's module system

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

Literature survey on improving type checker efficiency without altering the surface language

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.<br/><br/>This study aims to provide an explorative overview of proposed efficiency improvements for type checkers. This provides language implementers insight in what...

Dependent Types and Conversion Checking: A literature survey on implementation techniques for type systems

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

Literature survey of type inference algorithms for statically typed languages

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

Literature survey on implementation techniques for type systems: Exploring name binding techniques

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

Literature survey on implementation techniques for type systems: Inductive data types and pattern matching: What are the different implementation techniques for type systems regarding inductive data types and pattern matching that have been proposed in the literature?

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

Tactics in Agda using reflection

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