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函数的完整功能正确性。