Comparing Code extraction from Agda to Java to existing Methods

Bachelor thesis (2022)

Authors

L.K. Zimmerhackl Electrical Engineering, Mathematics and Computer Science

Contributors

J.G.H. Cockx Programming Languages - EEMCS (supervisor 1)
L.F.B. Escot Programming Languages - EEMCS (supervisor 2)
Faculty
Electrical Engineering, Mathematics and Computer Science
Copyright: © 2022 Lukas Zimmerhackl
Agda Java Code Extraction Agda2Java Compilation
More Info
expand_more

Published Date

27-06-2022

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Faculty

Electrical Engineering, Mathematics and Computer Science

Abstract

Dependent programming languages such as Agda show a lot of promise in creating new ways of writing code, but currently suffer from a lack of support and features. In this paper we attempt to create a new back-end for Agda targeting Java which has a huge and thriving ecosystem.

We implement the new back-end for Agda in Haskell and we describe the benefits and drawbacks of targeting Java. Firstly we go into the existing methods of compiler Agda, then we go into how to compile Agda to Java and what the main challenges where creating the compiler and what solutions were implemented to solve these. Afterwards Agda2Java is compared to the existing methods of compiling Agda code by means of benchmarks and analyzing the execution time. We show that at its current state, Java does not seem to be a promising back-end for Agda, but that there is work being done on Java that might change this perception.