Print Email Facebook Twitter Agda2Rust: A Study on an Alternative Backend for the Agda Compiler Title Agda2Rust: A Study on an Alternative Backend for the Agda Compiler Author Peeters, Hector (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 Agda is a functional programming language with built-in support for dependent types. A dependent type depends on a value. This allows the developer to specify strict constraints for the types used in an application. Writing code with dependent types results in fewer type-related errors slipping through the compilation process. When executing Agda code, it is first compiled into a different programming language. This process is called code extraction. This step is applied since most of the typed code becomes unnecessary after type-checking and can therefore be removed. Currently, the Agda compiler supports only Haskell and JavaScript as target languages. However, exploring Rust as a target language could potentially lead to better performance, and it would allow access to the Rust library ecosystem. Overall, the agda2rust backend could be a viable alternative to what is currently available. While it is not fully feature-complete and will not outperform any existing backends yet, agda2rust provides a way to seamlessly integrate algorithms and data structures implemented and proven in Agda into an existing Rust codebase. Subject Code ExtractionDependent TypesAgdaRust To reference this document use: http://resolver.tudelft.nl/uuid:39bff395-1bd6-4905-8554-cef0cd5e7d3e Part of collection Student theses Document type bachelor thesis Rights © 2022 Hector Peeters Files PDF paper_2.pdf 249.66 KB Close viewer /islandora/object/uuid:39bff395-1bd6-4905-8554-cef0cd5e7d3e/datastream/OBJ/view