References & Citations
Computer Science > Programming Languages
Title: Seamless, Correct, and Generic Programming over Serialised Data
(Submitted on 20 Oct 2023 (v1), last revised 26 Apr 2024 (this version, v2))
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.
Submission history
From: Guillaume Allais [view email][v1] Fri, 20 Oct 2023 12:09:17 GMT (55kb)
[v2] Fri, 26 Apr 2024 16:18:36 GMT (122kb)
Link back to: arXiv, form interface, contact.