• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Formalization on Modern Coding Theory

Research Project

Project/Area Number 25289118
Research Category

Grant-in-Aid for Scientific Research (B)

Allocation TypePartial Multi-year Fund
Section一般
Research Field Communication/Network engineering
Research InstitutionChiba University

Principal Investigator

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

Co-Investigator(Kenkyū-buntansha) Reynald Affeldt  国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (40415641)
KASAI Kenta  東京工業大学, 理工学研究科, 准教授 (70431997)
KUZUOKA Shigeaki  和歌山大学, システム工学部, 准教授 (60452538)
Garrigue Jacques  名古屋大学, 多元数理科学研究科, 准教授 (80273530)
Co-Investigator(Renkei-kenkyūsha) MIZOGUCHI Yoshihiro  九州大学, マス・フォア・インダストリ研究所, 准教授 (80209783)
Research Collaborator NATION James B.  
OBI Ryosuke  
NAKANO Kyosuke  
SAIKAWA Takafumi  
Project Period (FY) 2013-04-01 – 2016-03-31
Project Status Completed (Fiscal Year 2015)
Budget Amount *help
¥17,030,000 (Direct Cost: ¥13,100,000、Indirect Cost: ¥3,930,000)
Fiscal Year 2015: ¥6,500,000 (Direct Cost: ¥5,000,000、Indirect Cost: ¥1,500,000)
Fiscal Year 2014: ¥6,760,000 (Direct Cost: ¥5,200,000、Indirect Cost: ¥1,560,000)
Fiscal Year 2013: ¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
Keywords形式化 / 情報理論 / 符号理論 / LDPC符号 / 誤り訂正符号 / LDPC符号 / 空間結合LDPC符号 / モダン符号理論 / マスデジタリゼーション / モダン符号 / 密度発展法 / ssreflect / Coq / 型理論 / 疎
Outline of Final Research Achievements

To formalize modern coding theory, our research formalized "(spatially coupled) LDPC codes", "sum-product decoding algorithm" and related topics and also developed related theories. For example, we formalized channel capacities over BEC and BSEC, properties of stopping set, and Reed-Solomong codes and Euclidean decoding algorithm. We have organized workshops and open our result through web-sites.

Report

(4 results)
  • 2015 Annual Research Report   Final Research Report ( PDF )
  • 2014 Annual Research Report
  • 2013 Annual Research Report
  • Research Products

    (46 results)

All 2016 2015 2014 2013 Other

All Int'l Joint Research (1 results) Journal Article (16 results) (of which Int'l Joint Research: 2 results,  Peer Reviewed: 9 results,  Open Access: 3 results,  Acknowledgement Compliant: 5 results) Presentation (22 results) (of which Int'l Joint Research: 9 results,  Invited: 5 results) Remarks (6 results) Funded Workshop (1 results)

  • [Int'l Joint Research] University of Hawaii(米国)

    • Related Report
      2015 Annual Research Report
  • [Journal Article] A short proof for the multi-deletion error correction property of Helberg codes2016

    • Author(s)
      Manabu Hagiwara
    • Journal Title

      IEICE Communications Express

      Volume: 5 Issue: 2 Pages: 49-51

    • DOI

      10.1587/comex.2015XBL0182

    • NAID

      130005125260

    • ISSN
      2187-0136
    • Related Report
      2015 Annual Research Report
    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Journal Article] Uniqueness of Buston Hadamard matrices of small degrees2015

    • Author(s)
      M.Hirasaka, K.Kim, Y.Mizoguchi
    • Journal Title

      Journal of Discrete Algorithms

      Volume: 34 Pages: 70-77

    • Related Report
      2015 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] A Property of Random Walks on a Cycle Graph2015

    • Author(s)
      Y.Ikeda, Y.Fukai, Y.Mizoguchi
    • Journal Title

      Pacific Journal of Mathematics for Industry

      Volume: 7 Issue: 1

    • DOI

      10.1186/s40736-015-0015-3

    • NAID

      40020727637

    • Related Report
      2015 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] 順序のある代数系上の挿入削除誤り訂正符号2015

    • Author(s)
      萩原学
    • Journal Title

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

      Volume: 1 Pages: 469-474

    • Related Report
      2015 Annual Research Report
    • Acknowledgement Compliant
  • [Journal Article] Coq/SSReflectによる二元消失通信路の通信路容量の形式化2015

    • Author(s)
      中野恭輔、萩原学
    • Journal Title

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

      Volume: 1 Pages: 752-757

    • Related Report
      2015 Annual Research Report
    • Acknowledgement Compliant
  • [Journal Article] Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory2015

    • Author(s)
      Reynald Affeldt, Jacques Garrigue
    • Journal Title

      Springer LNCS

      Volume: 9236 Pages: 17-33

    • DOI

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

    • ISBN
      9783319221014, 9783319221021
    • Related Report
      2015 Annual Research Report
    • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
  • [Journal Article] Variable-Length Coding for Mixed Sources with Side Information Allowing Decoding Errors2015

    • Author(s)
      Shigeaki Kuzuoka
    • Journal Title

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

      Volume: 1 Pages: 51-58

    • Related Report
      2015 Annual Research Report
    • Acknowledgement Compliant
  • [Journal Article] Formalization of Error-correcting Codes using SSReflect2015

    • Author(s)
      Reynald Affeldt, Jacques Garrigue
    • Journal Title

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

      Volume: 61 Pages: 76-78

    • Related Report
      2014 Annual Research Report
  • [Journal Article] On formalization of basic geometric topology2015

    • Author(s)
      Ken’ichi Kuga, Manabu Hagiwara
    • Journal Title

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

      Volume: 61 Pages: 110-114

    • Related Report
      2014 Annual Research Report
  • [Journal Article] Formalization of the Variable-Length Source Coding Theorem: Direct Part2014

    • Author(s)
      Ryosuke Obi, Manabu Hagiwara, and Reynald Affeldt
    • Journal Title

      Proceeding of International Symposium on Information Theory and its Applications

      Volume: 1 Pages: 201-205

    • Related Report
      2014 Annual Research Report
    • Peer Reviewed
  • [Journal Article] A Certified Implementation of ML with Structural Polymorphism2014

    • Author(s)
      Jacques Garrigue
    • Journal Title

      Mathematical Structures in Computer Science

      Volume: December issue

    • Related Report
      2013 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Formalization of Shannon's Theorems Using the Coq Proof-Assistant2014

    • Author(s)
      Reynald Affeldt, Manabu Hagiwara, Jonas Senizergues
    • Journal Title

      Journal of Automated Reasoning

      Volume: 紙版、印刷中 Issue: 1 Pages: 63-103

    • DOI

      10.1007/s10817-013-9298-1

    • Related Report
      2013 Annual Research Report
    • Peer Reviewed
  • [Journal Article] SFA-LDPC符号の同値性2013

    • Author(s)
      萩原学, J.B.Nation
    • Journal Title

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

      Volume: 1 Pages: 163-168

    • Related Report
      2013 Annual Research Report
  • [Journal Article] Weight Distribution for Non-binary Cluster LDPC Code Ensemble2013

    • Author(s)
      T.Nozaki, K.Kasai, and K.Sakaniwa
    • Journal Title

      IEICE Trans. on Fundamentals

      Volume: E96-A Pages: 2382-2390

    • NAID

      130003385287

    • Related Report
      2013 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Achieving Near Capacity of Non-Binary LDPC Coded Large MIMO Systems with a Novel Ultra Low-Complexitity Soft-Output Detector2013

    • Author(s)
      P.Suthisopapan, K.Kasai, A.Meesomboon, and V.Imwawil
    • Journal Title

      IEEE Trans. on Wireless Communications

      Volume: vol12, no.10 Issue: 10 Pages: 5185-5199

    • DOI

      10.1109/twc.2013.090513.122056

    • Related Report
      2013 Annual Research Report
  • [Journal Article] Multi-Dimensional Spatially-Coupled Codes2013

    • Author(s)
      R. Ohashi, K. Kasai, and K. Takeuch
    • Journal Title

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

      Volume: 1 Pages: 2448-2452

    • DOI

      10.1109/isit.2013.6620666

    • Related Report
      2013 Annual Research Report
    • Peer Reviewed
  • [Presentation] A Mathematica module for Conformal Geometric Algebra and Origami Folding2016

    • Author(s)
      M.Kondo, T.Matsuo, Y.Mizoguchi, H.Ochiai,
    • Organizer
      SCSS 2016. 7th International Symposium on Symbolic Computation in Software Science
    • Place of Presentation
      お茶の水女子大学(東京都・文京区)
    • Year and Date
      2016-03-28
    • Related Report
      2015 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Workshop on Formalization of Applied Mathematical Systems2016

    • Author(s)
      T.Matsushima, Y.Mizoguchi, A.D.Jourdan
    • Organizer
      SCSS 2016. 7th International Symposium on Symbolic Computation in Software Science
    • Place of Presentation
      お茶の水女子大学(東京都・文京区)
    • Year and Date
      2016-03-28
    • Related Report
      2015 Annual Research Report
    • Int'l Joint Research
  • [Presentation] 二元消失通信路のシャノン限界形式化とその形式的証明について2015

    • Author(s)
      中野恭輔
    • Organizer
      平成27年度情報理論特別講演会
    • Place of Presentation
      休暇村紀州加太(和歌山県・和歌山市)
    • Year and Date
      2015-12-18
    • Related Report
      2015 Annual Research Report
  • [Presentation] 多重挿入/削除誤り訂正符号の順序付代数による構成とその表現2015

    • Author(s)
      萩原学
    • Organizer
      琉球大学理学部セミナー
    • Place of Presentation
      琉球大学(沖縄県・中頭郡)
    • Year and Date
      2015-12-04
    • Related Report
      2015 Annual Research Report
    • Invited
  • [Presentation] 多重挿入/削除誤り訂正符号の構成と表現2015

    • Author(s)
      萩原学
    • Organizer
      実験計画法と符号および関連する組合せ構造
    • Place of Presentation
      箱根水明荘(神奈川県・足柄下郡)
    • Year and Date
      2015-12-01
    • Related Report
      2015 Annual Research Report
    • Invited
  • [Presentation] Wang Tiles Modeling of Wall Patterns2015

    • Author(s)
      A.D.Jourdan, Y.Mizoguchi and M.Salvati
    • Organizer
      Mathematical Progress in Expressive Image Systems (MEIS2015)
    • Place of Presentation
      九州大学(福岡県福岡市)
    • Year and Date
      2015-09-25
    • Related Report
      2015 Annual Research Report
    • Int'l Joint Research
  • [Presentation] A Coq Library for the Theory of Realational Calculus2015

    • Author(s)
      Y.Mizoguchi
    • Organizer
      Workshop on Formalization of Applied Mathematical Systems
    • Place of Presentation
      Honolulu (米国)
    • Year and Date
      2015-09-25
    • Related Report
      2015 Annual Research Report
    • Int'l Joint Research / Invited
  • [Presentation] Formalization of the Channel Capacity of Binary Erasure Channel in Coq/SSReflect2015

    • Author(s)
      Kyosuke Nakano
    • Organizer
      Workshop on Formalization of Applied Mathematical Systems
    • Place of Presentation
      Honolulu (米国)
    • Year and Date
      2015-09-25
    • Related Report
      2015 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Certification of a sum-product algorithm for LDPC on a BSC2015

    • Author(s)
      Jacques Garrigue
    • Organizer
      Workshop on Formalization of Applied Mathematical Systems
    • Place of Presentation
      Honolulu (米国)
    • Year and Date
      2015-09-25
    • Related Report
      2015 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory2015

    • Author(s)
      Reynald Affeldt, Jacques Garrigue
    • Organizer
      Workshop on Formalization of Applied Mathematical Systems
    • Place of Presentation
      Honolulu (米国)
    • Year and Date
      2015-09-25
    • Related Report
      2015 Annual Research Report
    • Int'l Joint Research
  • [Presentation] GADTs and exhaustiveness: looking for the impossible2015

    • Author(s)
      Jacques Garrigue, Jacques Le Normand
    • Organizer
      ML Family Workshop
    • Place of Presentation
      Vancouver (カナダ)
    • Year and Date
      2015-09-03
    • Related Report
      2015 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory2015

    • Author(s)
      Reynald Affeldt, Jacques Garrigue
    • Organizer
      The 6th conference on Interactive Theorem Proving
    • Place of Presentation
      Nanjing (中国)
    • Year and Date
      2015-08-24
    • Related Report
      2015 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory2015

    • Author(s)
      Reynald Affeldt, Jacques Garrigue
    • Organizer
      Marelle Project Seminar, INRIA
    • Place of Presentation
      Sophia Antipolis, France
    • Year and Date
      2015-03-31
    • Related Report
      2014 Annual Research Report
  • [Presentation] 可変長情報源符号化逆定理の形式化2014

    • Author(s)
      小尾良介, 萩原学, 山本光晴
    • Organizer
      SITA2014
    • Place of Presentation
      富山県宇奈月ニューオータニホテル
    • Year and Date
      2014-12-09 – 2014-12-12
    • Related Report
      2014 Annual Research Report
  • [Presentation] 可変長情報源符号化定理の形式化の改良2014

    • Author(s)
      萩原学, 小尾良介
    • Organizer
      SITA2014
    • Place of Presentation
      富山県宇奈月ニューオータニホテル
    • Year and Date
      2014-12-09 – 2014-12-12
    • Related Report
      2014 Annual Research Report
  • [Presentation] Formalization of Error-correcting Codes using SSReflect2014

    • Author(s)
      Reynald Affeldt, Jacques Garrigue
    • Organizer
      研究集会「高信頼な理論と実装のための定理証明および定理証明器」
    • Place of Presentation
      九州大学
    • Year and Date
      2014-12-03 – 2014-12-05
    • Related Report
      2014 Annual Research Report
  • [Presentation] Formalization of Error-correcting Codes using SSReflect2014

    • Author(s)
      Reynald Affeldt, Jacques Garrigue
    • Organizer
      The 6th Coq Workshop
    • Place of Presentation
      Vienna, Austria
    • Year and Date
      2014-07-18
    • Related Report
      2014 Annual Research Report
  • [Presentation] Spatially-Coupled MacKay-Neal Codes with No Bit Nodes of Degree Two Achieve the Capacity of BEC2014

    • Author(s)
      Takuya Okazaki, Kenta Kasai
    • Organizer
      2014 IEEE International Symposium on Information Theory
    • Place of Presentation
      Honolulu, Hawaii
    • Year and Date
      2014-06-29 – 2014-07-04
    • Related Report
      2014 Annual Research Report
  • [Presentation] Spatially-Coupled Precoded Rateless Codes with Bounded Degree Achieve the Capacity of BEC under BP decoding2014

    • Author(s)
      Kosuke Sakata, Kenta Kasai, Kohichi Sakaniwa
    • Organizer
      2014 IEEE International Symposium on Information Theory
    • Place of Presentation
      Honolulu, Hawaii
    • Year and Date
      2014-06-29 – 2014-07-04
    • Related Report
      2014 Annual Research Report
  • [Presentation] 空間結合符号とその研究動向2014

    • Author(s)
      笠井健太
    • Organizer
      電子情報通信学会総合大会
    • Place of Presentation
      新潟大学
    • Related Report
      2013 Annual Research Report
  • [Presentation] Formalization of Shannon's Theorems Using the Coq Proof-Assistant2013

    • Author(s)
      Reynald Affeldt
    • Organizer
      2013年電子情報通信学会 ソサイエティ大会
    • Place of Presentation
      福岡工業大学
    • Related Report
      2013 Annual Research Report
    • Invited
  • [Presentation] Spatially Coupled Codes2013

    • Author(s)
      笠井 健太
    • Organizer
      Workshop on Modern Error Correcting Codes
    • Place of Presentation
      東京大学
    • Related Report
      2013 Annual Research Report
    • Invited
  • [Remarks] infotheoライブラリ

    • URL

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

    • Related Report
      2015 Annual Research Report
  • [Remarks] 雅利賀 惹玖のホームページ

    • URL

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

    • Related Report
      2015 Annual Research Report
  • [Remarks] Linear ECCs in Coq

    • URL

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

    • Related Report
      2015 Annual Research Report
  • [Remarks] Formalization of Shannon's Theorems

    • URL

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

    • Related Report
      2014 Annual Research Report
  • [Remarks] TPP2014

    • URL

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

    • Related Report
      2014 Annual Research Report
  • [Remarks] Formalization of VL Source Coding Theorem

    • URL

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

    • Related Report
      2013 Annual Research Report
  • [Funded Workshop] Workshop on Formalization of Applied Mathematical Systems2015

    • Place of Presentation
      University of Hawaii
    • Year and Date
      2015-09-25
    • Related Report
      2015 Annual Research Report

URL: 

Published: 2013-05-21   Modified: 2022-01-27  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi