Dependently typed languages such as Agda have the potential to revolutionize the way we write software because they allow the programmer to catch more bugs at compile time than classical languages. Nonetheless, dependently typed languages are hardly used in practice. One of the reasons is the lack of mature compilers for them. This paper describes the implementation of a new Agda compiler that targets the Higher-Order Virtual Machine (HVM). Firstly we outline the theoretical benefits of using an optimal functional language such as HVM. Secondly, we present the problems we faced and the solutions we devised in the implementation of the agda2hvm compiler. Lastly, we compare our implementation to the current best Agda compilers by running benchmarks and analyzing both time and space performance. We obtained results ranging from our compiler being exponentially faster than the state-of-the-art to being exponentially slower.

XMM is a newly designed multi-execution memory model that solves the out-of-thin-air exe- cutions problem, enables the most efficient compilation to all hardware platforms, and allows common compiler optimizations. Promising and Weakestmo are similar multi-execution models proposed recently. However, due to their complex semantics, they do not have an accompany- ing model checker with a proof of soundness. XMM is significantly less complex, which paved the way for implementing an XMM model checker. In our work, we present our design of a model checker algorithm for the XMM memory model called GenMC-XMM. Due to practical limitations of algorithmic time complexity, we could not design a complete model checker. However, we provide a proof of soundness. In other words, we cannot guarantee that our tool will find all possible executions of a program, but we can guarantee that the ones it finds are all XMM consistent. To our knowledge, GenMC-XMM is the first multi-execution model checker proven to be sound. We evaluated our tool against the state-of-the-art model checking tools for RC11, IMM, and Weakestmo2. We determined that GenMC-XMM explores the same or more executions than every other tool in all our tests. GenMC-XMM is only marginally slower than the other tools in real-world lock-free data- structure benchmarks. In synthetic tests designed to have thousands of data races, GenMC- XMM does not scale as well as the other tools as the number of races increases. GenMC-XMM is the next milestone in the automatic verification of multi-execution memory models. Based on our work on GenMC-XMM, other researchers may improve its performance and design a sound and complete algorithm.