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.

This paper extends the Multi-Agent Pathfinding (MAPF) algorithm, A*+ID+OD, to be able to solve problems with matching. This extension still keeps the optimal and completeness properties of the original algorithm. Matching is added to the algorithm in both an exhaustive and heuristic manner. Exhaustive matching is further improved by adding a new layer of Independence Detection (ID) to reduce the number of matchings. Besides this, the pruning efficiency is increased by sorting the matchings based on the initial heuristic. The exhaustive matching method has been found to perform better than the heuristic matching method. The exhaustive version of A*+ID+OD is finally compared to other extended MAPF algorithms which shows that on small maps, Conflict Based Min-Cost Flow (CBM) performs best as it is the only algorithm that does not use exhaustive matching. A*+ID+OD and Enhanced Partial Expansion A* (EPEA*) also perform well on open maps with multiple teams when compared to other exhaustive matching algorithms due to the addition of matching ID.