Implementing and Optimizing a Simple, Dependently-Typed Language

Examensarbete för masterexamen

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12380/124826
Download file(s):
File Description SizeFormat 
124826.pdfFulltext294 kBAdobe PDFView/Open
Type: Examensarbete för masterexamen
Master Thesis
Title: Implementing and Optimizing a Simple, Dependently-Typed Language
Authors: Blaguszewski, Michael
Abstract: This thesis presents a compiler for the simple functional programming language LambdaPi, which includes dependent types. The compiler is written in Haskell and uses LLVM, a framework for building optimizing compiler backends. It can compile the complete standard library provided by LambdaPi’s authors into native machine code. It is not much of an optimizing compiler, but several obvious opportunities for improvement exist. First I discuss the theoretical background of project: the principles of dependent types and the languages which include them. I also give a brief overview of the LLVM system and of related work. The second section describes the process of implementation, which was done in stages from a trivial calculator language up to full LambdaPi. And finally we consider opportunities for optimization. Some of these stem from Edwin Brady’s [2005] analysis of Epigram, while others are lower-level and can be performed for us by LLVM.
Keywords: Datalogi;Computer science
Issue Date: 2010
Publisher: Chalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)
Chalmers University of Technology / Department of Computer Science and Engineering (Chalmers)
URI: https://hdl.handle.net/20.500.12380/124826
Collection:Examensarbeten för masterexamen // Master Theses



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.