Data Layout from a Type-Theoretic Perspective

Reference. Data Layout from a Type-Theoretic Perspective

Henry DeYoung, Frank Pfenning · ENTCS · 2023 · DOI · arXiv

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.

Cite

Cite as @deyoung-2023-data (helia, typst) · \cite{deyoung-2023-data} (LaTeX)

BibTeX

bibtex · 1 line

@article{deyoung-2023-data, title={Data Layout from a Type-Theoretic Perspective}, volume={1}, ISSN={2969-2431}, url={http://dx.doi.org/10.46298/entics.10507}, DOI={10.46298/entics.10507}, journal={Electronic Notes in Theoretical Informatics and Computer Science}, publisher={Centre pour la Communication Scientifique Directe (CCSD)}, author={DeYoung, Henry and Pfenning, Frank}, year={2023}, month=Feb }

hayagriva YAML (typst)

yaml · 16 lines

deyoung-2023-data:
  type: article
  title: Data Layout from a Type-Theoretic Perspective
  author:
  - DeYoung, Henry
  - Pfenning, Frank
  date: 2023-02
  url: http://dx.doi.org/10.46298/entics.10507
  serial-number:
    doi: 10.46298/entics.10507
    issn: 2969-2431
  parent:
    type: periodical
    title: Electronic Notes in Theoretical Informatics and Computer Science
    publisher: Centre pour la Communication Scientifique Directe (CCSD)
    volume: 1

Download: deyoung-2023-data.bib · deyoung-2023-data.yml

Cited by (2)

Dependent Type Refinements for Futures somayyajula-2023-dependentENTCS · 2023

Type refinements combine the compositionality of typechecking with the expressivity of program logics, offering a synergistic approach to program verification. In this paper we apply dependent type refinements to SAX, a futures-based process calculus that arises from the Curry-Howard interpretation of the intuitionistic semi-axiomatic sequent calculus and includes unrestricted recursion both at the level of types and processes. With our type refinement system, we can reason about the partial correctness of SAX programs, complementing prior work on sized type refinements that supports reasoning about termination. Our design regime synthesizes the infinitary proof theory of SAX with that of bidirectional typing and Hoare logic, deriving some standard reasoning principles for data and (co)recursion while enabling information hiding for codata. We prove syntactic type soundness, which entails a notion of partial correctness that respects codata encapsulation. We illustrate our language through a few simple examples.

DOI

Relating Message Passing and Shared Memory, Proof-Theoretically pfenning-2023-relatingCoordination Models and Languages · 2023

DOI

Cites 20 works (1 here)

With notes (1)

A mixed linear and non-linear logic: Proofs, terms and models: Extended abstract bentonMixedLinearNonlinear1995CSL · 1995

Intuitionistic linear logic regains the expressive power of intuitionistic logic through the ! (‘of course’) modality. Benton, Bierman, Hyland and de Paiva have given a term assignment system for ILL and an associated notion of categorical model in which the ! modality is modelled by a comonad satisfying certain extra conditions. Ordinary intuitionistic logic is then modelled in a cartesian closed category which arises as a full subcategory of the category of coalgebras for the comonad. This paper attempts to explain the connection between ILL and IL more directly and symmetrically by giving a logic, term calculus and categorical model for a system in which the linear and non-linear worlds exist on an equal footing, with operations allowing one to pass in both directions. We start from the categorical model of ILL given by Benton, Bierman, Hyland and de Paiva and show that this is equivalent to having a symmetric monoidal adjunction between a symmetric monoidal closed category and a cartesian closed category. We then derive both a sequent calculus and a natural deduction presentation of the logic corresponding to the new notion of model.

DOI

External (19)

Back to futures (2022)
Data layout from a type-theoretic perspective (extended version) (2022)
Semi-Axiomatic Sequent Calculus (2020)
Adjoint logic and its concurrent operational interpretation (unpublished manuscript) (2018)
A judgmental deconstruction of modal logic (unpublished manuscript) (2009)
A type theory for memory allocation and data layout (2003)
Call-By-Push-Value (Ph.D. thesis, University of London) (2001)
From system F to typed assembly language (1999)
On the meanings of the logical constants and the justifications of the logical laws (1996)
A λ-calculus structure isomorphic to Gentzen-style sequent calculus structure (1995)
On the unity of logic (1993)
Logic Programming with Focusing Proofs in Linear Logic (1992)
The Logical Basis of Metaphysics (1991)
MULTILISP: a language for concurrent symbolic computation (1985)
The formulae-as-types notion of construction (1980)
The incremental garbage collection of processes (1977)
Analytic cut (1969)
Untersuchungen über das logische Schließen. I (1935)
Functionality in Combinatory Logic (1934)