Towards a System-Level Functional Language: Lithium

Abstract

Functional programming has a rich and well-documented history. In functional programming, large problems can be described by the composition of smaller building blocks. Despite its benefits, functional programming has struggled to find its way into system-level programming. By leveraging the guarantees linear types impose, functional programming languages can be applied to system-level programming without sacrificing performance.

This thesis presents Lithium, a system-level functional programming language that is based on a variant of linear logic. Lithium is designed to be an intermediate compilation target for linear functional languages. We give the typing and kinding rules for Lithium before describing a series of transformations to turn Lithium into a language that is easily translated into assembly code. Additionally, we present a compilation scheme, a mapping from types to memory, and the application binary interface (ABI).