{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,31]],"date-time":"2024-10-31T03:08:54Z","timestamp":1730344134321,"version":"3.28.0"},"reference-count":13,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.23919\/isita.2018.8664276","type":"proceedings-article","created":{"date-parts":[[2019,3,11]],"date-time":"2019-03-11T23:49:11Z","timestamp":1552348151000},"page":"633-637","source":"Crossref","is-referenced-by-count":1,"title":["Examples of Formal Proofs about Data Compression"],"prefix":"10.23919","author":[{"given":"Reynald","family":"Affeldt","sequence":"first","affiliation":[]},{"given":"Jacques","family":"Garrigue","sequence":"additional","affiliation":[]},{"given":"Takafumi","family":"Saikawa","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"journal-title":"The Coq Proof Assistant","year":"0","key":"ref10"},{"journal-title":"Mathematical Components Libraries of formalized mathematics","year":"0","key":"ref11"},{"year":"0","author":"strub","key":"ref12"},{"journal-title":"The infotheo library","year":"0","key":"ref13"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9298-1"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9116-y"},{"key":"ref6","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/978-3-319-22102-1_2","article-title":"Formalization of error-correcting codes: from Hamming to modern coding theory","volume":"9236","author":"affeldt","year":"0","journal-title":"6th Conference on Interactive Theorem Proving (ITP 2015) LNCS"},{"key":"ref5","first-page":"201","article-title":"Formalization of variable-length source coding theorem: Direct part","author":"obi","year":"0","journal-title":"International Symposium on Information Theory and Its Applications (ISITA 2014)"},{"key":"ref8","first-page":"537","article-title":"Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes","author":"affeldt","year":"0","journal-title":"International Symposium on Information Theory and Its Applications (ISITA 2016)"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_37"},{"journal-title":"Elements of Information Theory","year":"2006","author":"cover","key":"ref2"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511606267"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316588284"}],"event":{"name":"2018 International Symposium on Information Theory and Its Applications (ISITA)","start":{"date-parts":[[2018,10,28]]},"location":"Singapore","end":{"date-parts":[[2018,10,31]]}},"container-title":["2018 International Symposium on Information Theory and Its Applications (ISITA)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8660385\/8664205\/08664276.pdf?arnumber=8664276","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,27]],"date-time":"2022-01-27T06:20:27Z","timestamp":1643264427000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8664276\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10]]},"references-count":13,"URL":"https:\/\/doi.org\/10.23919\/isita.2018.8664276","relation":{},"subject":[],"published":{"date-parts":[[2018,10]]}}}