Implementing and Optimizing a Simple, Dependently-Typed Language
Ladda ner
Typ
Examensarbete för masterexamen
Master Thesis
Master Thesis
Program
Publicerad
2010
Författare
Blaguszewski, Michael
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
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.
Beskrivning
Ämne/nyckelord
Datalogi , Computer science