Compilers are edging towards more advanced compilation techniques, a huge factor limiting advances in compilers is the type system of programming languages. Within the last five years the integration of dependent type ...