文献

J-GLOBAL ID：202002275840629280   整理番号：20A1634593

線形誤り訂正符号の形式化のためのライブラリ【JST・京大機械翻訳】

A Library for Formalization of Linear Error-Correcting Codes

著者 (3件)： Affeldt Reynald (Cyber Physical Security Research Center, National Institute of Advanced Industrial Science and Technology (AIST), Tsukuba, Japan) ,  Garrigue Jacques (Graduate School of Mathematics, Nagoya University, Nagoya, Japan) ,  Saikawa Takafumi (Graduate School of Mathematics, Nagoya University, Nagoya, Japan)
資料名： Journal of Automated Reasoning  (Journal of Automated Reasoning)
巻： 64  号： 6  ページ： 1123-1164  発行年： 2020年 
JST資料番号： D0269E  ISSN： 0168-7433  CODEN： JAREEW  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 誤り訂正符号は,雑音の多いチャネル上の信頼できる通信を確保するために,送信データに冗長性を加える。それらはディジタル通信の基礎を形成するので,それらの正当性は懸念の問題である。線形誤り訂正符号の信頼できる検証を可能にするために,Coq証明支援における系統的定式化を行った。この形式化は,トピックに関する大学クラスを期待できる材料を含む:よく知られたコード(Hamming,Reed-Solomon,Bose-Chaudhuri-Hocquenghem)の形式化,および現代の符号化理論におけるグリムプス。和積アルゴリズムに基づく低密度パリティ検査符号のための検証復号器を抽出することによって,著者らの形式化の有用性を実証した。この形式化を達成するために,著者らはCoqの数学的構成要素のトップに関して多くのライブラリを開発する必要があった。将来における誤り訂正コードを扱う実装者と研究者を支援するように,それらをできるだけ再利用できるように,特別な注意を払った。Copyright Springer Nature B.V. 2020 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： アルゴリズム ,  雑音 ,  冗長性 ,  ディジタル通信 ,  復号器 ,  符号理論 ,  線形性 ,  再利用 ,  チャネル ,  定式化 ,  *誤り訂正符号
準シソーラス用語： LDPC符号 , 【Automatic Indexing@JST】

著者キーワード (3件)： Coq ,  数学部品 ,  誤り訂正符号

分類 (1件)： 符号理論  (ND02030R)

タイトルに関連する用語 (4件)： 線形 ,  誤り訂正符号 ,  形式化 ,  ライブラリ