Henry DeYoung ; Frank Pfenning - Data Layout from a Type-Theoretic Perspective

entics:10507 - Electronic Notes in Theoretical Informatics and Computer Science, February 22, 2023, Volume 1 - Proceedings of MFPS XXXVIII - https://doi.org/10.46298/entics.10507
Data Layout from a Type-Theoretic PerspectiveArticle

Authors: Henry DeYoung ; Frank Pfenning

    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.


    Volume: Volume 1 - Proceedings of MFPS XXXVIII
    Published on: February 22, 2023
    Accepted on: December 20, 2022
    Submitted on: December 20, 2022
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages

    1 Document citing this article

    Consultation statistics

    This page has been seen 267 times.
    This article's PDF has been downloaded 151 times.