In Named-Data Networking (NDN), all packets are encoded in the Type-Length-Value (TLV) format. TLV encoding and decoding are implemented in every NDN library, and used by all applications and forwarders. Therefore, formal analysis of TLV encoding can assist NDN software development in the simplification of the code base, analysis of the performance, and improvement of robustness. In this paper, we want to bring attention to the subtleties of TLV encoding. As an initial result, we develop a type-theoretical model of TLV encodable types, and give an algorithm to automatically derive encoding and decoding functions. We formally prove that the derived encoding and decoding functions are inverse to each other. To evaluate the practicality of automatically derived algorithms, we implement the proposed algorithms in C++ templates and evaluate them in three aspects: performance, memory usage, and code complexity. Our results show that our C++ library is competitive in these three aspects. Though our implementation is not fully automated, we show that it is possible to have a fully automated library in future that correctly produce the encoding and decoding functions. We also discussed the limitations of our model and problems worth attention. We hope our work can offer a starting point of further research on TLV, especially formal analysis and automated implementation.
