Typer la d\'e-s\'erialisation sans s\'erialiser les types

TL;DR

This paper introduces a method for static type assignment to unmarshalling functions, ensuring safe data deserialization through a verified technique using singleton types and an efficient runtime checking algorithm.

Contribution

It presents a novel verification approach for unmarshalled data that maintains static type safety, proven correct and capable of handling sharing and cycles.

Findings

Verification technique is proven correct

Efficient algorithm handles sharing and cycles

Ensures execution safety in deserialization

Abstract

In this paper, we propose a way of assigning static type information to unmarshalling functions and we describe a verification technique for unmarshalled data that preserves the execution safety provided by static type checking. This technique, whose correctness is proven, relies on singleton types whose values are transmitted to unmarshalling routines at runtime, and on an efficient checking algorithm able to deal with sharing and cycles.