Writing software that follows its specification is important for many applications. One approach to guarantee this is formal verification in a dependently-typed programming language. Formal verification in these dependently-typed languages is based on proof writing. Sadly, while proofs are easy to check for computers, writing proofs can be tedious for developers. One particular proof component that currently requires developers attention in many systems, is associative and commutative (AC) reasoning.
We contribute an extension of dependent type-systems to fully automate AC reasoning. This alleviates developers from this task and allows them to concentrate on other proof components. Our approach works by modifying the conversion checker and doesn't compromise soundness or completeness. Furthermore, our approach reuses existing type-checking components, making it easier to implement. We also implemented our theory as an extension of the Agda type-checker. This allowed us to use this implementation to experiment with some example programs.
This thesis can help language designers decide if they want automatic AC reasoning in their language. For language users it can serve as inspiration on how to use such a type-system and finally for researchers we have ideas for future work.

FPT algorithms for cluster editing are relatively successful in practice, however there is still the need for a fast weighted graph data-structure that allows merging vertices and deleting edges while keeping track of a lower bound. This paper presents such a data-structure with at worst O(n²) time complexities for basic operations on graphs with n vertices. Furthermore an open-source implementation of the data-structure and an algorithm for cluster editing is provided, written in Rust for performance and readability.