Towards a Practical Execution Model for Functional Languages with Linear Types

Abstract

Typed functional programming has an attractive logical foundation which ensures safety and modularity. System-level programming, on the other hand, offers finegrained control over program execution. Is there a way to combine those two strengths? In this thesis, we take a first step in compiling functional languages to a C-like paradigm. Specifically, we propose a functional compiler intermediate language designed to bridge the gap between high-level functional programming and low-level system programming. To retain the generality of functional programming while allowing for finer control, we adopt a modular design where higher-level features decompose into lower-level constructs within a shared language. Our design is not solely driven by practical considerations but rather we achieve memory control by following the structure of linear logic. In fact, our language is heavily based on the proof structure of a sequent calculus presentation of linear logic. In leveraging this formal system, our language gain theoretical interest and many desirable properties while simultaneously enabling a more direct execution model. To demonstrate the viability of our design, we compile our language into a virtual machine language. The virtual machine language, which is specifically design as a target for our intermediate language, has an assembly-like style that maps naturally onto existing computer architecture. This suggest the potential for compiling our language into actual machine code. Given that this work represents an initial effort of compiling functional languages to a C-like paradigm, we do not address all aspects of language design. Our primary contribution focuses on the treatment of functions, with particular emphasis on their representation and calling conventions.