Tanaka Akira 田中哲

… Alternative Names

田中哲タナカアキラ

TANAKA Akira 田中哲

Less

Researcher Number	10357452
Other IDs
External Links
Affiliation (Current)	2025: 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員
Affiliation (based on the past Project Information) *help	2024: 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 2017: 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 2015 – 2016: 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 2003: National Institute of Advanced Inductrial Science and Technology, Information Technology Research Institute, Researcher, 情報処理研究部門, 研究員
Review Section/Research Field	Except Principal Investigator Basic Section 60050:Software-related / Software / Science and Engineering
Keywords	Except Principal Investigator 統計 / プログラム検証 / 形式手法 / コード生成器 / プログラミング言語C / プログラミング言語OCaml / 簡潔データ構造 / 定理証明支援系 / metalevel architecuture / object-oriented language … More / byte-code modification / software composition / dynamic adaptation / mobile code / runtime checking / policy enforcement / ロード時自己反映 / 適応可能ソフトウェア / 拡張可能ソフトウェア / 安全なソフトウェア / Java / 契約による設計 / アスペクト / 形式仕様 / JML / 自己反映計算 / セキュリティポリシー / セキュリティ / メタレベルアーキテクチャ / オブジェクト指向言語 / バイトコード変換 / モジュール結合 / 動的適応 / 移動コード / 実行時検査 / ポリシー強制 Less

Formal verification methods for trustworthy statistics
- Principal Investigator
  
  川本裕輔
- Project Period (FY)
  2024 – 2026
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Review Section
  
  Basic Section 60050:Software-related
- Research Institution
  National Institute of Advanced Industrial Science and Technology
Towards formal verification of big data processing
- Principal Investigator
  
  AFFELDT Reynald
- Project Period (FY)
  2015 – 2017
- Research Category
  
  Grant-in-Aid for Challenging Exploratory Research
- Research Field
  
  Software
- Research Institution
  National Institute of Advanced Industrial Science and Technology
Secure Construction Methods for Extensible and Adaptable Software
- Principal Investigator
  
  WATANABE Takuo
- Project Period (FY)
  2000 – 2003
- Research Category
  
  Grant-in-Aid for Scientific Research on Priority Areas
- Review Section
  
  Science and Engineering
- Research Institution
  National Institute of Informatics
  Tokyo Institute of Technology

All 2018 2017 2016

All Journal Article Presentation

[Journal Article] Safe Low-level Code Generation in Coq Using Monomorphization and Monadification2018
- Author(s)
  Tanaka Akira、Affeldt Reynald、Garrigue Jacques
- Journal Title
  
  Journal of Information Processing
  
  Volume: 26 Issue: 0 Pages: 54-72
- DOI
  10.2197/ipsjjip.26.54
- NAID
  130006309263
- ISSN
  1882-6652
- Language
  English
- Peer Reviewed / Open Access / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-15K12013
[Journal Article] Formal Verification of the rank Function for Succinct Data Structures2016
- Author(s)
  Akira Tanaka, Reynald Affeldt, Jacques Garrigue
- Journal Title
  
  Proceedings of the 18th JSSST Workshop on Programming and Programming Languages
  
  Volume: 1 Pages: 1-15
- Peer Reviewed / Acknowledgement Compliant / Open Access
- Data Source
  KAKENHI-PROJECT-15K12013
[Journal Article] Formal Verification of the rank Algorithm for Succinct Data Structures2016
- Author(s)
  Akira Tanaka, Reynald Affeldt, and Jacques Garrigue
- Journal Title
  
  Lecture Notes in Computer Science
  
  Volume: 10009 Pages: 243-260
- DOI
  10.1007/978-3-319-47846-3_16
- ISBN
  9783319478456, 9783319478463
- Peer Reviewed / Acknowledgement Compliant
- Data Source
  KAKENHI-PROJECT-15K12013
[Presentation] Coqによる簡潔データ構造のライブラリに向けての今後の課題2017
- Author(s)
  田中哲, Reynald Affeldt, Jacques Garrigue
- Organizer
  第20回プログラミングおよびプログラミング言語ワークショップ（PPL2018）
- Data Source
  KAKENHI-PROJECT-15K12013
[Presentation] Ruby Extension Library Verified using Coq Proof-assistant2017
- Author(s)
  田中哲
- Organizer
  RubyKaigi 2017
- Data Source
  KAKENHI-PROJECT-15K12013
[Presentation] Coq からの C プログラム生成2017
- Author(s)
  田中哲
- Organizer
  Proof Summit 2017
- Data Source
  KAKENHI-PROJECT-15K12013
[Presentation] Safe Low-level Code Generation in Coq using Monomorphization and Monadification2017
- Author(s)
  田中哲，Reynald Affeldt，Jacques Garrigue
- Organizer
  情報処理学会プログラミング研究会第114回プログラミング研究発表会
- Data Source
  KAKENHI-PROJECT-15K12013
[Presentation] Coq からの低レベル C コード生成2017
- Author(s)
  田中哲
- Organizer
  The 13th Theorem Proving and Provers Meeting (TPP 2017)
- Data Source
  KAKENHI-PROJECT-15K12013
[Presentation] Certified Mon{omorphiz|adific}ation of Gallina for Low-level Code Extraction2017
- Author(s)
  田中哲, Reynald Affeldt, Jacques Garrigue
- Organizer
  第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）
- Place of Presentation
  華やぎの章慶山ホテル山梨県笛吹市
- Year and Date
  2017-03-09
- Data Source
  KAKENHI-PROJECT-15K12013
[Presentation] Formal Verification of the rank Function for Succinct Data Structures2016
- Author(s)
  Akira Tanaka, Reynald Affeldt, Jacques Garrigue
- Organizer
  18th JSSST Workshop on Programming and Programming Languages
- Place of Presentation
  ダイヤモンド瀬戸内マリンホテル(岡山県玉野市)
- Year and Date
  2016-03-08
- Data Source
  KAKENHI-PROJECT-15K12013
[Presentation] Formal Verification of the rank Algorithm for Succinct Data Structures2016
- Author(s)
  Akira Tanaka, Reynald Affeldt, and Jacques Garrigue
- Organizer
  18th International Conference on Formal Engineering Methods (ICFEM 2016), November 14-18, 2016
- Place of Presentation
  TKP Ichigaya Conference Center, Tokyo
- Year and Date
  2016-11-17
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-15K12013

1. WATANABE Takuo (20222408)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
2. ISCHISUGI Yuuji (30356464)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
3. GONDOW Katsuhiko (50262283)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
4. AMANO Noriki (30313703)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
5. SUZUKI Masato (30242572)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
6. AFFELDT Reynald (40415641)

# of Collaborated Projects: 1 results

# of Collaborated Products: 7 results
7. J Garrigue (80273530)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
8. 川本裕輔 (60760006)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
9. 末永幸平 (70633692)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
10. 佐藤哲也 (40761797)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
11. GAARUGUE Jacques

# of Collaborated Projects: 0 results

# of Collaborated Products: 7 results

Tanaka Akira 田中 哲

田中 哲 タナカ アキラ

TANAKA Akira 田中 哲

Research Projects

Research Products

Co-Researchers

Formal verification methods for trustworthy statistics

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Towards formal verification of big data processing

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Secure Construction Methods for Extensible and Adaptable Software

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

[Journal Article] Safe Low-level Code Generation in Coq Using Monomorphization and Monadification2018

Author(s)

Journal Title

DOI

NAID

ISSN

Language

Data Source

[Journal Article] Formal Verification of the rank Function for Succinct Data Structures2016

Author(s)

Journal Title

Data Source

[Journal Article] Formal Verification of the rank Algorithm for Succinct Data Structures2016

Author(s)

Journal Title

DOI

ISBN

Data Source

[Presentation] Coqによる簡潔データ構造のライブラリに向けての今後の課題2017

Author(s)

Organizer

Data Source

[Presentation] Ruby Extension Library Verified using Coq Proof-assistant2017

Author(s)

Organizer

Data Source

[Presentation] Coq からの C プログラム生成2017

Author(s)

Organizer

Data Source

[Presentation] Safe Low-level Code Generation in Coq using Monomorphization and Monadification2017

Author(s)

Organizer

Data Source

[Presentation] Coq からの低レベル C コード生成2017

Author(s)

Organizer

Data Source

[Presentation] Certified Mon{omorphiz|adific}ation of Gallina for Low-level Code Extraction2017

Author(s)

Organizer

Place of Presentation

Year and Date

Data Source

[Presentation] Formal Verification of the rank Function for Succinct Data Structures2016

Author(s)

Organizer

Place of Presentation

Year and Date

Data Source

[Presentation] Formal Verification of the rank Algorithm for Succinct Data Structures2016

Author(s)

Organizer

Place of Presentation

Year and Date

Data Source

Tanaka Akira 田中哲

田中哲タナカアキラ

TANAKA Akira 田中哲