Bringing Classical Sequent Calculus to The Web
When choosing a compiler intermediate representation, both its intrinsic properties and the availability of compilation targets must be considered. It should admit an easy translation from a rich surface language, be type-safe, and make strong meta-theoretical guarantees. AxCut has recently been proposed in this field, meeting these requirements. It inherits the logical properties from classical sequent calculus and can elegantly model complex control flow. However, an intermediate representation is only relevant if it can be used to generate machine code for the architectures of interest. While AxCut can already be compiled to x86-64 and AArch64, one increasingly important target is currently missing: the web. In this thesis, we enable users of AxCut to target browsers. We therefore provide a translation from AxCut to WebAssembly. WebAssembly strongly differs from the classical architec tures AxCut was originally designed for. Despite this, we reproduce the semantics while matching the native code in terms of the number and types of jumps. To ensure correctness, our implementation was tested extensively and enforces certain invariants using dependent types. Preliminary performance evaluations show that performance is not yet comparable to the native code, but we provide potential solutions for this.