田中哲 Tanaka Akira

研究者番号	10357452
その他のID
外部サイト
所属 (現在)	2025年度: 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員
所属 (過去の研究課題情報に基づく) *注記	2024年度 – 2025年度: 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 2017年度: 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 2015年度 – 2016年度: 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 2003年度: 産業技術総合研究所, 情報処理研究部門, 研究員
審査区分/研究分野	研究代表者以外小区分60050:ソフトウェア関連 / ソフトウェア / 理工系
キーワード	研究代表者以外定理証明支援系 / 計算効果 / 関数型プログラミング言語 / 等式理論 / 統計 / プログラム検証 / 形式手法 / コード生成器 / プログラミング言語C / プログラミング言語OCaml … もっと見る / 簡潔データ構造 / metalevel architecuture / object-oriented language / byte-code modification / software composition / dynamic adaptation / mobile code / runtime checking / policy enforcement / ロード時自己反映 / 適応可能ソフトウェア / 拡張可能ソフトウェア / 安全なソフトウェア / Java / 契約による設計 / アスペクト / 形式仕様 / JML / 自己反映計算 / セキュリティポリシー / セキュリティ / メタレベルアーキテクチャ / オブジェクト指向言語 / バイトコード変換 / モジュール結合 / 動的適応 / 移動コード / 実行時検査 / ポリシー強制隠す

計算効果を持つプログラムの証明のための枠組みの構築
- 研究代表者
  
  J Garrigue
- 研究期間 (年度)
  2025 – 2028
- 研究種目
  
  基盤研究(B)
- 審査区分
  
  小区分60050:ソフトウェア関連
- 研究機関
  名古屋大学
信頼できる統計のための形式検証技術
- 研究代表者
  
  川本裕輔
- 研究期間 (年度)
  2024 – 2026
- 研究種目
  
  基盤研究(B)
- 審査区分
  
  小区分60050:ソフトウェア関連
- 研究機関
  国立研究開発法人産業技術総合研究所
ビッグデータ処理の形式検証に向けて
- 研究代表者
  
  Affeldt Reynald
- 研究期間 (年度)
  2015 – 2017
- 研究種目
  
  挑戦的萌芽研究
- 研究分野
  
  ソフトウェア
- 研究機関
  国立研究開発法人産業技術総合研究所
拡張・適応可能なソフトウェアのセキュアな構成方式
- 研究代表者
  
  渡部卓雄
- 研究期間 (年度)
  2000 – 2003
- 研究種目
  
  特定領域研究
- 審査区分
  
  理工系
- 研究機関
  国立情報学研究所
   東京工業大学

すべて 2018 2017 2016

すべて雑誌論文学会発表

[雑誌論文] Safe Low-level Code Generation in Coq Using Monomorphization and Monadification2018
- 著者名/発表者名
  Tanaka Akira、Affeldt Reynald、Garrigue Jacques
- 雑誌名
  
  Journal of Information Processing
  
  巻: 26 号: 0 ページ: 54-72
- DOI
  10.2197/ipsjjip.26.54
- NAID
  130006309263
- ISSN
  1882-6652
- 言語
  英語
- 査読あり / オープンアクセス / 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-15K12013
[雑誌論文] Formal Verification of the rank Function for Succinct Data Structures2016
- 著者名/発表者名
  Akira Tanaka, Reynald Affeldt, Jacques Garrigue
- 雑誌名
  
  Proceedings of the 18th JSSST Workshop on Programming and Programming Languages
  
  巻: 1 ページ: 1-15
- 査読あり / 謝辞記載あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-15K12013
[雑誌論文] Formal Verification of the rank Algorithm for Succinct Data Structures2016
- 著者名/発表者名
  Akira Tanaka, Reynald Affeldt, and Jacques Garrigue
- 雑誌名
  
  Lecture Notes in Computer Science
  
  巻: 10009 ページ: 243-260
- DOI
  10.1007/978-3-319-47846-3_16
- ISBN
  9783319478456, 9783319478463
- 査読あり / 謝辞記載あり
- データソース
  KAKENHI-PROJECT-15K12013
[学会発表] Coqによる簡潔データ構造のライブラリに向けての今後の課題2017
- 著者名/発表者名
  田中哲, Reynald Affeldt, Jacques Garrigue
- 学会等名
  第20回プログラミングおよびプログラミング言語ワークショップ（PPL2018）
- データソース
  KAKENHI-PROJECT-15K12013
[学会発表] Ruby Extension Library Verified using Coq Proof-assistant2017
- 著者名/発表者名
  田中哲
- 学会等名
  RubyKaigi 2017
- データソース
  KAKENHI-PROJECT-15K12013
[学会発表] Coq からの C プログラム生成2017
- 著者名/発表者名
  田中哲
- 学会等名
  Proof Summit 2017
- データソース
  KAKENHI-PROJECT-15K12013
[学会発表] Safe Low-level Code Generation in Coq using Monomorphization and Monadification2017
- 著者名/発表者名
  田中哲，Reynald Affeldt，Jacques Garrigue
- 学会等名
  情報処理学会プログラミング研究会第114回プログラミング研究発表会
- データソース
  KAKENHI-PROJECT-15K12013
[学会発表] Coq からの低レベル C コード生成2017
- 著者名/発表者名
  田中哲
- 学会等名
  The 13th Theorem Proving and Provers Meeting (TPP 2017)
- データソース
  KAKENHI-PROJECT-15K12013
[学会発表] Certified Mon{omorphiz|adific}ation of Gallina for Low-level Code Extraction2017
- 著者名/発表者名
  田中哲, Reynald Affeldt, Jacques Garrigue
- 学会等名
  第19回プログラミングおよびプログラミング言語ワークショップ（PPL2017）
- 発表場所
  華やぎの章慶山ホテル山梨県笛吹市
- 年月日
  2017-03-09
- データソース
  KAKENHI-PROJECT-15K12013
[学会発表] Formal Verification of the rank Function for Succinct Data Structures2016
- 著者名/発表者名
  Akira Tanaka, Reynald Affeldt, Jacques Garrigue
- 学会等名
  18th JSSST Workshop on Programming and Programming Languages
- 発表場所
  ダイヤモンド瀬戸内マリンホテル(岡山県玉野市)
- 年月日
  2016-03-08
- データソース
  KAKENHI-PROJECT-15K12013
[学会発表] Formal Verification of the rank Algorithm for Succinct Data Structures2016
- 著者名/発表者名
  Akira Tanaka, Reynald Affeldt, and Jacques Garrigue
- 学会等名
  18th International Conference on Formal Engineering Methods (ICFEM 2016), November 14-18, 2016
- 発表場所
  TKP Ichigaya Conference Center, Tokyo
- 年月日
  2016-11-17
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-15K12013

1. Affeldt Reynald (40415641)

共同の研究課題数: 2件

共同の研究成果数: 7件
2. J Garrigue (80273530)

共同の研究課題数: 2件

共同の研究成果数: 0件
3. 渡部卓雄 (20222408)

共同の研究課題数: 1件

共同の研究成果数: 0件
4. 一杉裕志 (30356464)

共同の研究課題数: 1件

共同の研究成果数: 0件
5. 権藤克彦 (50262283)

共同の研究課題数: 1件

共同の研究成果数: 0件
6. 天野憲樹 (30313703)

共同の研究課題数: 1件

共同の研究成果数: 0件
7. 鈴木正人 (30242572)

共同の研究課題数: 1件

共同の研究成果数: 0件
8. 川本裕輔 (60760006)

共同の研究課題数: 1件

共同の研究成果数: 0件
9. 末永幸平 (70633692)

共同の研究課題数: 1件

共同の研究成果数: 0件
10. 佐藤哲也 (40761797)

共同の研究課題数: 1件

共同の研究成果数: 0件
11. 才川隆文 (00897100)

共同の研究課題数: 1件

共同の研究成果数: 0件
12. 勝股審也 (30378963)

共同の研究課題数: 1件

共同の研究成果数: 0件
13. GAARUGUE Jacques

共同の研究課題数: 0件

共同の研究成果数: 7件

田中 哲 Tanaka Akira

研究課題

研究成果

共同研究者

計算効果を持つプログラムの証明のための枠組みの構築

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

信頼できる統計のための形式検証技術

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

ビッグデータ処理の形式検証に向けて

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

拡張・適応可能なソフトウェアのセキュアな構成方式

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

[雑誌論文] Safe Low-level Code Generation in Coq Using Monomorphization and Monadification2018

著者名/発表者名

雑誌名

DOI

NAID

ISSN

言語

データソース

[雑誌論文] Formal Verification of the rank Function for Succinct Data Structures2016

著者名/発表者名

雑誌名

データソース

[雑誌論文] Formal Verification of the rank Algorithm for Succinct Data Structures2016

著者名/発表者名

雑誌名

DOI

ISBN

データソース

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

著者名/発表者名

学会等名

データソース

[学会発表] Ruby Extension Library Verified using Coq Proof-assistant2017

著者名/発表者名

学会等名

データソース

[学会発表] Coq からの C プログラム生成2017

著者名/発表者名

学会等名

データソース

[学会発表] Safe Low-level Code Generation in Coq using Monomorphization and Monadification2017

著者名/発表者名

学会等名

データソース

[学会発表] Coq からの低レベル C コード生成2017

著者名/発表者名

学会等名

データソース

[学会発表] Certified Mon{omorphiz|adific}ation of Gallina for Low-level Code Extraction2017

著者名/発表者名

学会等名

発表場所

年月日

データソース

[学会発表] Formal Verification of the rank Function for Succinct Data Structures2016

著者名/発表者名

学会等名

発表場所

年月日

データソース

[学会発表] Formal Verification of the rank Algorithm for Succinct Data Structures2016

著者名/発表者名

田中哲 Tanaka Akira