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.

翻译：在类型化函数式语言中，通常只有在将数据先反序列化为内存中的树形结构（其中节点以结构体表示、子项以指针表示）后，才能以类型安全的方式对其进行操作。我们演示了如何利用 Idris 中实现的量子类型理论（QTT）来定义序列化数据类型的微型宇宙，并提供通用程序，使用户能够处理连续存储在缓冲区中的值。我们的方法允许实现者通过构造的方式证明处理缓冲区中存储数据的IO函数的完全功能正确性。