Data Layout from a Type-Theoretic Perspective

TL;DR

This paper introduces a type-theoretic framework for data layout in functional programming, aiming to improve efficiency and control by formalizing data structures and addresses within a logical semantics.

Contribution

It develops a novel type-theoretic approach based on sequent calculus semantics to model and refine data layouts with recursive types for compiler and programming control.

Findings

Formal semantics for data layout using sequent calculus

Refinement of address structures to reflect alternative layouts

Exploration of recursive types and their properties

Abstract

The specifics of data layout can be important for the efficiency of functional programs and interaction with external libraries. In this paper, we develop a type-theoretic approach to data layout that could be used as a typed intermediate language in a compiler or to give a programmer more control. Our starting point is a computational interpretation of the semi-axiomatic sequent calculus for intuitionistic logic that defines abstract notions of cells and addresses. We refine this semantics so addresses have more structure to reflect possible alternative layouts without fundamentally departing from intuitionistic logic. We then add recursive types and explore example programs and properties of the resulting language.