Summary
The 2018 International Symposium on Information Theory and Its Applications (ISITA2018)
2018
Session Number:We-PM-1-3
Session:
Number:We-PM-1-3.1
Examples of Formal Proofs about Data Compression
Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa,
pp.665-669
Publication Date:2018/10/18
Online ISSN:2188-5079
DOI:10.34385/proc.55.We-PM-1-3.1
PDF download
Summary:
Because of the increasing complexity of mathematical proofs, there is a growing interest in formalization using proof-assistants. In this paper, we explain new formal proofs of standard lemmas in data compression (Jensen’s and Kraft’s inequalities) as well as concrete applications (to the analysis of compression methods and Shannon-Fano codes). We explain in particular how one turns the paper proof into formal terms and the relation between the informal proof and the formal one. These formalizations come as an extension to an existing formal library for information theory and error-correcting codes.