Code extraction from Agda to HVM

Title

Code extraction from Agda to HVM

 Author

Meluzzi, Matteo (TU Delft Electrical Engineering, Mathematics and Computer Science; TU Delft Programming Languages)

Contributor

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

Degree granting institution

Delft University of Technology

 Programme

Computer Science and Engineering

 Project

CSE3000 Research Project

 Date

2022-06-27

 Abstract

Dependently typed languages such as Agda have the potential to revolutionize the way we write software because they allow the programmer to catch more bugs at compile time than classical languages. Nonetheless, dependently typed languages are hardly used in practice. One of the reasons is the lack of mature compilers for them.
This paper describes the implementation of a new Agda compiler that targets the Higher-Order Virtual Machine (HVM). Firstly we outline the theoretical benefits of using an optimal functional language such as HVM. Secondly, we present the problems we faced and the solutions we devised in the implementation of the agda2hvm compiler. Lastly, we compare our implementation to the current best Agda compilers by running benchmarks and analyzing both time and space performance. We obtained results ranging from our compiler being exponentially faster than the state-of-the-art to being exponentially slower.

 Subject

Dependent Types
Compiler
Code Extraction
Agda
Interaction Nets

 To reference this document use:

http://resolver.tudelft.nl/uuid:90e4331b-d684-4578-ac14-5e448411b536

 Part of collection

Student theses

 Document type

bachelor thesis

 Rights

© 2022 Matteo Meluzzi
Files
PDF paper_thesis.pdf 757.59 KB
Close viewer