In early June I submitted the final revision of my Bachelor’s thesis, with the potentially impenetrable title “Compiling Agda to System Fω in Theory”.

I wrote this thesis under the supervision of Andreas Abel (Chalmers University of Technology), who is one of the main Agda implementers.

Abstract:

We develop a theoretical foundation for compiling the programming language Agda to System Fω, which is a stepping stone towards a compiler from Agda to Haskell. The practical relevance for software engineering and the problem of providing correctness guarantees for programs is highlighted. After describing relevant λ-calculi, we specify the semantics for compiling Agda to System Fω. Finally, we illustrate those compilation rules by manually translating several Agda code examples to System Fω.

The full paper is available here:
http://gregorulm.com/files/GregorUlm.BSc.FinalRevision.pdf