Seamless, correct, and generic programming over serialised data

Allais, Guillaume (2023) Seamless, correct, and generic programming over serialised data. Other. arXiv, Ithaca, NY. (https://doi.org/10.48550/arXiv.2310.13441)

[thumbnail of Allais-arXiv-2023-Seamless-correct-and-generic-programming-over-serialised-data]
Preview
 Text. Filename: Allais-arXiv-2023-Seamless-correct-and-generic-programming-over-serialised-data.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (368kB)| Preview

Abstract

In typed functional languages, one can typically only manipulate data in a type-safe manner if it first has been deserialised into an in-memory tree represented as a graph of nodes-as-structs and subterms-as-pointers. We demonstrate how we can use QTT as implemented in \idris{} to define a small universe of serialised datatypes, and provide generic programs allowing users to process values stored contiguously in buffers. Our approach allows implementors to prove the full functional correctness by construction of the IO functions processing the data stored in the buffer.

ORCID iDs

Allais, Guillaume ORCID logoORCID: https://orcid.org/0000-0002-4091-657X;
  • Item type:Monograph(Other)
    ID code:88778
    Dates:
    Date
    Event
    20 October 2023
    Published
    Subjects:Science > Mathematics > Electronic computers. Computer science
    Department:UNSPECIFIED
    Depositing user: Pure Administrator
    Date deposited:17 Apr 2024 15:48
    Last modified:20 Nov 2024 01:41
    URI:https://strathprints.strath.ac.uk/id/eprint/88778
CORE (COnnecting REpositories)