Print Email Facebook Twitter Extracting LLVM Intermediate Representation from Agda Title Extracting LLVM Intermediate Representation from Agda Author Broekhoff, Jochem (TU Delft Electrical Engineering, Mathematics and Computer Science) 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 Agda, a promising dependently typed function language, needs more mainstream adoption. By the process of code extraction, we compile proven Agda code into a popular existing language, allowing smooth integration with existing workflows. Due to Agda’s pluggable nature, this process is relatively straightforward. We implement a solution in Haskell and perform an empirical benchmark analysis. We show that LLVM’s Intermediate Representation language is a usable and promising target, although some optimizations are necessary before broader application. More indirect paths towards LLVM IR appear more suitable, because of the large translation gap. Subject code extractionAgdabackendLLVM Intemediate Representation To reference this document use: http://resolver.tudelft.nl/uuid:6ed6ad26-18c3-4427-b99a-c6241f7102c7 Part of collection Student theses Document type bachelor thesis Rights © 2022 Jochem Broekhoff Files PDF agda2llvm.pdf 638.54 KB Close viewer /islandora/object/uuid:6ed6ad26-18c3-4427-b99a-c6241f7102c7/datastream/OBJ/view