Initially present only in functional languages such as OCaml and Haskell, Algebraic Data Types have now become pervasive in mainstream languages, providing nice data abstractions and an elegant way to express functions through pattern matching. Unfortunately, ADTs remain seldom
used in low-level programming. One reason is that their increased convenience comes at the cost of abstracting away the exact memory layout of values. Even Rust, which tries to optimize data layout, severely limits control over memory representation.
The goal of this thesis is to let programmers specify highly optimized memory layouts for inductive data structures in a flexible and expressive way, while still enjoying high-level programming constructs such as ADTs and pattern matching to manipulate this data.
To this end, we propose a language dubbed ribbit which combines a high-level language, consisting of ADTs, pattern matching and basic manipulation of immutable values, with memory types specifying the precise memory layout of each high-level type, providing full control over the memory representation of values. We provide formal semantics of both (high-level and memory) languages which, together with agreement criteria stating the relationship between an ADT and a suitable memory layout, let us reason easily about values as they are represented in memory.
We then propose a compilation algorithm for the ribbit language which enables optimized compilation of pattern matching and code for arbitrary mangled memory representations, and emits CFG-style programs with explicit memory allocation and full support for recursive types.
Gratuit
Disciplines