Compiling classical sequent calculus to LLVM

This thesis aims to provide a way to translate classical sequent calculus to the LLVM intermediate representation to utilize the LLVM toolchain and achieve greater performance than compiling directly to machine code. We provide examples of how this translation works, what the resulting optimized version looks like and how and why we implemented a custom memory allocater to suit our needs. We show how to evaluate the resulting programs and how we test the validity of the translation. Finally we benchmark our approach against other programming languages and compare the resulting performance.

Contact

Jonathan Brachthäuser

Philipp Schuster