Comparing Code extraction from Agda to Java to existing Methods

Title

Comparing Code extraction from Agda to Java to existing Methods

 Author

Zimmerhackl, Lukas (TU Delft Electrical Engineering, Mathematics and Computer Science; TU Delft Programming Languages)

Contributor

Cockx, J.G.H. (mentor)
Escot, L.F.B. (graduation committee)

Degree granting institution

Delft University of Technology

 Programme

Computer Science and Engineering

 Project

CSE3000 Research Project

 Date

2022-06-27

 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.

 Subject

Agda
Java
Agda2Java
Code Extraction
Compilation

 To reference this document use:

http://resolver.tudelft.nl/uuid:dc59471d-6956-450d-bbd7-733ae5ff3f92

 Part of collection

Student theses

 Document type

bachelor thesis

 Rights

© 2022 Lukas Zimmerhackl
Files
PDF final_paper_final_klaar_mooi.pdf 491.85 KB
Close viewer