2023/10/20 by Guillaume Allais, Allais, Guillaume · 1 citation
Computer Science · #D.2.4 #Distributed systems and fault tolerance #E.1 #F.3.1 #FOS: Computer and information sciences #Logic, programming, and type systems #Parallel Computing and Optimization Techniques #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2310.13441
openalex publication_date 2023/10/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.