• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

モダン符号の形式化

研究課題

研究課題/領域番号 25289118
研究種目

基盤研究(B)

配分区分一部基金
応募区分一般
研究分野 通信・ネットワーク工学
研究機関千葉大学

研究代表者

萩原 学  千葉大学, 理学(系)研究科(研究院), 准教授 (80415728)

研究分担者 AFFELDT Reynald (Affeldt Reynald)  国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (40415641)
笠井 健太  東京工業大学, 理工学研究科, 准教授 (70431997)
葛岡 成晃  和歌山大学, システム工学部, 准教授 (60452538)
J Garrigue  名古屋大学, 多元数理科学研究科, 准教授 (80273530)
連携研究者 溝口 佳寛  九州大学, マス・フォア・インダストリ研究所, 准教授 (80209783)
研究協力者 NATION James B.  
小尾 良介  
中野 恭輔  
才川 隆文  
研究期間 (年度) 2013-04-01 – 2016-03-31
研究課題ステータス 完了 (2015年度)
配分額 *注記
17,030千円 (直接経費: 13,100千円、間接経費: 3,930千円)
2015年度: 6,500千円 (直接経費: 5,000千円、間接経費: 1,500千円)
2014年度: 6,760千円 (直接経費: 5,200千円、間接経費: 1,560千円)
2013年度: 3,770千円 (直接経費: 2,900千円、間接経費: 870千円)
キーワード形式化 / 情報理論 / 符号理論 / LDPC符号 / 誤り訂正符号 / LDPC符号 / 空間結合LDPC符号 / モダン符号理論 / マスデジタリゼーション / モダン符号 / 密度発展法 / ssreflect / Coq / 型理論 / 疎
研究成果の概要

モダン符号の形式化研究として、LDPC符号やsum-product復号に関する定義や性質の形式化や理論の発展を行った。必要に応じ、関連する話題の形式化にも着手した。具体的には、誤り訂正の限界に関わる二元消失通信路やその拡張である二元対称消失通信路の通信路容量の形式化、Stopping Setに関する形式化、実装時にLDPC符号と組合せて用いられることの多いReed-Solomon符号の形式化などである。本研究では、研究成果の普及活動として、ホームページによる成果公開や、ワークショップの開催も行った。

報告書

(4件)
  • 2015 実績報告書   研究成果報告書 ( PDF )
  • 2014 実績報告書
  • 2013 実績報告書
  • 研究成果

    (46件)

すべて 2016 2015 2014 2013 その他

すべて 国際共同研究 (1件) 雑誌論文 (16件) (うち国際共著 2件、 査読あり 9件、 オープンアクセス 3件、 謝辞記載あり 5件) 学会発表 (22件) (うち国際学会 9件、 招待講演 5件) 備考 (6件) 学会・シンポジウム開催 (1件)

  • [国際共同研究] University of Hawaii(米国)

    • 関連する報告書
      2015 実績報告書
  • [雑誌論文] A short proof for the multi-deletion error correction property of Helberg codes2016

    • 著者名/発表者名
      Manabu Hagiwara
    • 雑誌名

      IEICE Communications Express

      巻: 5 号: 2 ページ: 49-51

    • DOI

      10.1587/comex.2015XBL0182

    • NAID

      130005125260

    • ISSN
      2187-0136
    • 関連する報告書
      2015 実績報告書
    • 査読あり / オープンアクセス / 謝辞記載あり
  • [雑誌論文] Uniqueness of Buston Hadamard matrices of small degrees2015

    • 著者名/発表者名
      M.Hirasaka, K.Kim, Y.Mizoguchi
    • 雑誌名

      Journal of Discrete Algorithms

      巻: 34 ページ: 70-77

    • 関連する報告書
      2015 実績報告書
    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] A Property of Random Walks on a Cycle Graph2015

    • 著者名/発表者名
      Y.Ikeda, Y.Fukai, Y.Mizoguchi
    • 雑誌名

      Pacific Journal of Mathematics for Industry

      巻: 7 号: 1

    • DOI

      10.1186/s40736-015-0015-3

    • NAID

      40020727637

    • 関連する報告書
      2015 実績報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] 順序のある代数系上の挿入削除誤り訂正符号2015

    • 著者名/発表者名
      萩原学
    • 雑誌名

      情報理論とその応用シンポジウム予稿集

      巻: 1 ページ: 469-474

    • 関連する報告書
      2015 実績報告書
    • 謝辞記載あり
  • [雑誌論文] Coq/SSReflectによる二元消失通信路の通信路容量の形式化2015

    • 著者名/発表者名
      中野恭輔、萩原学
    • 雑誌名

      情報理論とその応用シンポジウム予稿集

      巻: 1 ページ: 752-757

    • 関連する報告書
      2015 実績報告書
    • 謝辞記載あり
  • [雑誌論文] Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory2015

    • 著者名/発表者名
      Reynald Affeldt, Jacques Garrigue
    • 雑誌名

      Springer LNCS

      巻: 9236 ページ: 17-33

    • DOI

      10.1007/978-3-319-22102-1_2

    • ISBN
      9783319221014, 9783319221021
    • 関連する報告書
      2015 実績報告書
    • 査読あり / 国際共著 / 謝辞記載あり
  • [雑誌論文] Variable-Length Coding for Mixed Sources with Side Information Allowing Decoding Errors2015

    • 著者名/発表者名
      Shigeaki Kuzuoka
    • 雑誌名

      第9回シャノン理論ワークショップ予稿集

      巻: 1 ページ: 51-58

    • 関連する報告書
      2015 実績報告書
    • 謝辞記載あり
  • [雑誌論文] Formalization of Error-correcting Codes using SSReflect2015

    • 著者名/発表者名
      Reynald Affeldt, Jacques Garrigue
    • 雑誌名

      MI Lecture Note 研究集会 高信頼な理論と実装のための定理証明および定理証明器 (TPP2014), 九州大学, December 3--5, 2014

      巻: 61 ページ: 76-78

    • 関連する報告書
      2014 実績報告書
  • [雑誌論文] On formalization of basic geometric topology2015

    • 著者名/発表者名
      Ken’ichi Kuga, Manabu Hagiwara
    • 雑誌名

      MI Lecture Note 研究集会 高信頼な理論と実装のための定理証明および定理証明器 (TPP2014), 九州大学, December 3--5, 2014

      巻: 61 ページ: 110-114

    • 関連する報告書
      2014 実績報告書
  • [雑誌論文] Formalization of the Variable-Length Source Coding Theorem: Direct Part2014

    • 著者名/発表者名
      Ryosuke Obi, Manabu Hagiwara, and Reynald Affeldt
    • 雑誌名

      Proceeding of International Symposium on Information Theory and its Applications

      巻: 1 ページ: 201-205

    • 関連する報告書
      2014 実績報告書
    • 査読あり
  • [雑誌論文] A Certified Implementation of ML with Structural Polymorphism2014

    • 著者名/発表者名
      Jacques Garrigue
    • 雑誌名

      Mathematical Structures in Computer Science

      巻: December issue

    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] Formalization of Shannon's Theorems Using the Coq Proof-Assistant2014

    • 著者名/発表者名
      Reynald Affeldt, Manabu Hagiwara, Jonas Senizergues
    • 雑誌名

      Journal of Automated Reasoning

      巻: 紙版、印刷中 号: 1 ページ: 63-103

    • DOI

      10.1007/s10817-013-9298-1

    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] SFA-LDPC符号の同値性2013

    • 著者名/発表者名
      萩原学, J.B.Nation
    • 雑誌名

      第36回情報理論とその応用シンポジウム予稿集

      巻: 1 ページ: 163-168

    • 関連する報告書
      2013 実績報告書
  • [雑誌論文] Weight Distribution for Non-binary Cluster LDPC Code Ensemble2013

    • 著者名/発表者名
      T.Nozaki, K.Kasai, and K.Sakaniwa
    • 雑誌名

      IEICE Trans. on Fundamentals

      巻: E96-A ページ: 2382-2390

    • NAID

      130003385287

    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] Achieving Near Capacity of Non-Binary LDPC Coded Large MIMO Systems with a Novel Ultra Low-Complexitity Soft-Output Detector2013

    • 著者名/発表者名
      P.Suthisopapan, K.Kasai, A.Meesomboon, and V.Imwawil
    • 雑誌名

      IEEE Trans. on Wireless Communications

      巻: vol12, no.10 号: 10 ページ: 5185-5199

    • DOI

      10.1109/twc.2013.090513.122056

    • 関連する報告書
      2013 実績報告書
  • [雑誌論文] Multi-Dimensional Spatially-Coupled Codes2013

    • 著者名/発表者名
      R. Ohashi, K. Kasai, and K. Takeuch
    • 雑誌名

      2013 IEEE Int. Symp. Inf. Theory, Istanbul, Turkey

      巻: 1 ページ: 2448-2452

    • DOI

      10.1109/isit.2013.6620666

    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [学会発表] A Mathematica module for Conformal Geometric Algebra and Origami Folding2016

    • 著者名/発表者名
      M.Kondo, T.Matsuo, Y.Mizoguchi, H.Ochiai,
    • 学会等名
      SCSS 2016. 7th International Symposium on Symbolic Computation in Software Science
    • 発表場所
      お茶の水女子大学(東京都・文京区)
    • 年月日
      2016-03-28
    • 関連する報告書
      2015 実績報告書
    • 国際学会
  • [学会発表] Workshop on Formalization of Applied Mathematical Systems2016

    • 著者名/発表者名
      T.Matsushima, Y.Mizoguchi, A.D.Jourdan
    • 学会等名
      SCSS 2016. 7th International Symposium on Symbolic Computation in Software Science
    • 発表場所
      お茶の水女子大学(東京都・文京区)
    • 年月日
      2016-03-28
    • 関連する報告書
      2015 実績報告書
    • 国際学会
  • [学会発表] 二元消失通信路のシャノン限界形式化とその形式的証明について2015

    • 著者名/発表者名
      中野恭輔
    • 学会等名
      平成27年度情報理論特別講演会
    • 発表場所
      休暇村紀州加太(和歌山県・和歌山市)
    • 年月日
      2015-12-18
    • 関連する報告書
      2015 実績報告書
  • [学会発表] 多重挿入/削除誤り訂正符号の順序付代数による構成とその表現2015

    • 著者名/発表者名
      萩原学
    • 学会等名
      琉球大学理学部セミナー
    • 発表場所
      琉球大学(沖縄県・中頭郡)
    • 年月日
      2015-12-04
    • 関連する報告書
      2015 実績報告書
    • 招待講演
  • [学会発表] 多重挿入/削除誤り訂正符号の構成と表現2015

    • 著者名/発表者名
      萩原学
    • 学会等名
      実験計画法と符号および関連する組合せ構造
    • 発表場所
      箱根水明荘(神奈川県・足柄下郡)
    • 年月日
      2015-12-01
    • 関連する報告書
      2015 実績報告書
    • 招待講演
  • [学会発表] Wang Tiles Modeling of Wall Patterns2015

    • 著者名/発表者名
      A.D.Jourdan, Y.Mizoguchi and M.Salvati
    • 学会等名
      Mathematical Progress in Expressive Image Systems (MEIS2015)
    • 発表場所
      九州大学(福岡県福岡市)
    • 年月日
      2015-09-25
    • 関連する報告書
      2015 実績報告書
    • 国際学会
  • [学会発表] A Coq Library for the Theory of Realational Calculus2015

    • 著者名/発表者名
      Y.Mizoguchi
    • 学会等名
      Workshop on Formalization of Applied Mathematical Systems
    • 発表場所
      Honolulu (米国)
    • 年月日
      2015-09-25
    • 関連する報告書
      2015 実績報告書
    • 国際学会 / 招待講演
  • [学会発表] Formalization of the Channel Capacity of Binary Erasure Channel in Coq/SSReflect2015

    • 著者名/発表者名
      Kyosuke Nakano
    • 学会等名
      Workshop on Formalization of Applied Mathematical Systems
    • 発表場所
      Honolulu (米国)
    • 年月日
      2015-09-25
    • 関連する報告書
      2015 実績報告書
    • 国際学会
  • [学会発表] Certification of a sum-product algorithm for LDPC on a BSC2015

    • 著者名/発表者名
      Jacques Garrigue
    • 学会等名
      Workshop on Formalization of Applied Mathematical Systems
    • 発表場所
      Honolulu (米国)
    • 年月日
      2015-09-25
    • 関連する報告書
      2015 実績報告書
    • 国際学会
  • [学会発表] Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory2015

    • 著者名/発表者名
      Reynald Affeldt, Jacques Garrigue
    • 学会等名
      Workshop on Formalization of Applied Mathematical Systems
    • 発表場所
      Honolulu (米国)
    • 年月日
      2015-09-25
    • 関連する報告書
      2015 実績報告書
    • 国際学会
  • [学会発表] GADTs and exhaustiveness: looking for the impossible2015

    • 著者名/発表者名
      Jacques Garrigue, Jacques Le Normand
    • 学会等名
      ML Family Workshop
    • 発表場所
      Vancouver (カナダ)
    • 年月日
      2015-09-03
    • 関連する報告書
      2015 実績報告書
    • 国際学会
  • [学会発表] Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory2015

    • 著者名/発表者名
      Reynald Affeldt, Jacques Garrigue
    • 学会等名
      The 6th conference on Interactive Theorem Proving
    • 発表場所
      Nanjing (中国)
    • 年月日
      2015-08-24
    • 関連する報告書
      2015 実績報告書
    • 国際学会
  • [学会発表] Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory2015

    • 著者名/発表者名
      Reynald Affeldt, Jacques Garrigue
    • 学会等名
      Marelle Project Seminar, INRIA
    • 発表場所
      Sophia Antipolis, France
    • 年月日
      2015-03-31
    • 関連する報告書
      2014 実績報告書
  • [学会発表] 可変長情報源符号化逆定理の形式化2014

    • 著者名/発表者名
      小尾良介, 萩原学, 山本光晴
    • 学会等名
      SITA2014
    • 発表場所
      富山県宇奈月ニューオータニホテル
    • 年月日
      2014-12-09 – 2014-12-12
    • 関連する報告書
      2014 実績報告書
  • [学会発表] 可変長情報源符号化定理の形式化の改良2014

    • 著者名/発表者名
      萩原学, 小尾良介
    • 学会等名
      SITA2014
    • 発表場所
      富山県宇奈月ニューオータニホテル
    • 年月日
      2014-12-09 – 2014-12-12
    • 関連する報告書
      2014 実績報告書
  • [学会発表] Formalization of Error-correcting Codes using SSReflect2014

    • 著者名/発表者名
      Reynald Affeldt, Jacques Garrigue
    • 学会等名
      研究集会「高信頼な理論と実装のための定理証明および定理証明器」
    • 発表場所
      九州大学
    • 年月日
      2014-12-03 – 2014-12-05
    • 関連する報告書
      2014 実績報告書
  • [学会発表] Formalization of Error-correcting Codes using SSReflect2014

    • 著者名/発表者名
      Reynald Affeldt, Jacques Garrigue
    • 学会等名
      The 6th Coq Workshop
    • 発表場所
      Vienna, Austria
    • 年月日
      2014-07-18
    • 関連する報告書
      2014 実績報告書
  • [学会発表] Spatially-Coupled MacKay-Neal Codes with No Bit Nodes of Degree Two Achieve the Capacity of BEC2014

    • 著者名/発表者名
      Takuya Okazaki, Kenta Kasai
    • 学会等名
      2014 IEEE International Symposium on Information Theory
    • 発表場所
      Honolulu, Hawaii
    • 年月日
      2014-06-29 – 2014-07-04
    • 関連する報告書
      2014 実績報告書
  • [学会発表] Spatially-Coupled Precoded Rateless Codes with Bounded Degree Achieve the Capacity of BEC under BP decoding2014

    • 著者名/発表者名
      Kosuke Sakata, Kenta Kasai, Kohichi Sakaniwa
    • 学会等名
      2014 IEEE International Symposium on Information Theory
    • 発表場所
      Honolulu, Hawaii
    • 年月日
      2014-06-29 – 2014-07-04
    • 関連する報告書
      2014 実績報告書
  • [学会発表] 空間結合符号とその研究動向2014

    • 著者名/発表者名
      笠井健太
    • 学会等名
      電子情報通信学会総合大会
    • 発表場所
      新潟大学
    • 関連する報告書
      2013 実績報告書
  • [学会発表] Formalization of Shannon's Theorems Using the Coq Proof-Assistant2013

    • 著者名/発表者名
      Reynald Affeldt
    • 学会等名
      2013年電子情報通信学会 ソサイエティ大会
    • 発表場所
      福岡工業大学
    • 関連する報告書
      2013 実績報告書
    • 招待講演
  • [学会発表] Spatially Coupled Codes2013

    • 著者名/発表者名
      笠井 健太
    • 学会等名
      Workshop on Modern Error Correcting Codes
    • 発表場所
      東京大学
    • 関連する報告書
      2013 実績報告書
    • 招待講演
  • [備考] infotheoライブラリ

    • URL

      http://manau.jp/research/infotheo/

    • 関連する報告書
      2015 実績報告書
  • [備考] 雅利賀 惹玖のホームページ

    • URL

      http://www.math.nagoya-u.ac.jp/~garrigue/home-j.html

    • 関連する報告書
      2015 実績報告書
  • [備考] Linear ECCs in Coq

    • URL

      https://staff.aist.go.jp/reynald.affeldt/ecc/

    • 関連する報告書
      2015 実績報告書
  • [備考] Formalization of Shannon's Theorems

    • URL

      https://staff.aist.go.jp/reynald.affeldt/shannon/

    • 関連する報告書
      2014 実績報告書
  • [備考] TPP2014

    • URL

      http://imi.kyushu-u.ac.jp/lasm/tpp2014/index_ja.html

    • 関連する報告書
      2014 実績報告書
  • [備考] Formalization of VL Source Coding Theorem

    • URL

      https://github.com/Ryo8777/VLSCTheorem/blob/master/v_source_coding_direct.v

    • 関連する報告書
      2013 実績報告書
  • [学会・シンポジウム開催] Workshop on Formalization of Applied Mathematical Systems2015

    • 発表場所
      University of Hawaii
    • 年月日
      2015-09-25
    • 関連する報告書
      2015 実績報告書

URL: 

公開日: 2013-05-21   更新日: 2022-01-27  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi