Izumi Asakura

I am a Ph.D. student at Department of Mathematical and Computing Science, Tokyo Institute of Technology. My supervisor is Hidehiko Masuhara.


I am interested in the following topics.

  • DSLs for high-performance computing: especially, I am interested in the design, implementation and verification for DSLs for GPGPU.

I am developing CertSkel, a Formally verified Coq-embedded skeleton-based GPGPU DSL.


  1. 超解像処理におけるAccelerateプログラムのオーバーヘッドとその解消
    朝倉 泉, 増原 英彦, 松本 拓也,松崎 公紀
    第114回プログラミング研究発表会, 静岡, 2017年6月, 査読なし
  2. Kani-CUDAによるGPGPUプログラムの合成
    蟹 暁, 朝倉 泉, 増原 英彦, 青谷 知幸
    第19回プログラミングおよびプログラミング言語ワークショップ (PPL2017), 山梨, 2017年3月, ポスター発表
  3. 検証済みコンパイラ CertSkel による GPGPU プログラム開発
    朝倉 泉, 増原 英彦, 青谷 知幸
    第19回プログラミングおよびプログラミング言語ワークショップ (PPL2017), 山梨, 2017年3月, ポスター発表
  4. バリア同期と共有メモリを備えたGPGPUプログラム合成器Kani-CUDA
    蟹 暁, 朝倉 泉, 増原 英彦, 青谷 知幸
    第113回プログラミング研究発表会, 東京, 2017年3月, 査読なし
  5. CertSkel: a Verified Compiler for a Coq-embedded GPGPU DSL
    Izumi Asakura, Hidehiko Masuhara, Tomoyuki Aotani.
    The Third International Workshop on Coq for Programming Languages (CoqPL 2017), co-located with The 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), Paris, France, January 2017
    (PDF file)
  6. Towards a Formally Verified Skeleton-based Data Parallel DSL for GPGPU
    Izumi Asakura, Hidehiko Masuhara, Tomoyuki Aotani.
    14th Asian Symposium on Programming Languages and Systems (APLAS 2016), Hanoi, Vietnam, November 2016, poster presentation
    Poster: (PDF file) (PPTX file)
  7. GPGPU向けデータ並列コードテンプレートの形式検証
    朝倉泉, 増原英彦, 青谷知幸
    第18回プログラミングおよびプログラミング言語ワークショップ (PPL2016), 岡山, 2016年3月, 登壇発表, 査読あり
    (PDF file)
  8. Proof of Soundness of Concurrent Separation Logic for GPGPU in Coq
    Izumi Asakura, Hidehiko Masuhara, Tomoyuki Aotani
    Journal of Information Processing Vol.24 No.1 132–140 (2016)
    (PDF file)
  9. GPGPU のための並行分離論理のCoq による健全性証明
    朝倉泉,増原英彦, 青谷知幸
    情報処理学会第104 回プログラミング研究発表会 (PRO-2015-1), 富山, 2015 年6月
  10. GPGPUカーネル検証のための分離論理のCoqによる形式化
    朝倉泉, 増原英彦, 青谷知幸
    第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015), 愛媛, 2015年3月, ポスター発表
  11. シェルコマンドを型安全に利用するための領域特化言語OCommand
    朝倉泉, 増原英彦, 青谷知幸
    日本ソフトウェア科学会第31回大会, 愛知, 2014年9月, ポスター発表
  12. OCommand : OCaml上の型安全なシェルプログラミングのための領域特化言語の提案
    朝倉泉, 増原英彦, 青谷知幸
    情報処理学会 第99回プログラミング研究発表会 (PRO-2014-1), 北海道, 2014年6月, 登壇発表, 査読なし
  13. 型安全なシェルプログラミングのための領域特化言語の提案
    朝倉泉, 増原英彦, 青谷知幸
    第16回プログラミングおよびプログラミング言語ワークショップ (PPL2014), 熊本, 2014年3月, ポスター発表
  14. OCamlのシェルプログラミングのための安全な領域特化言語の提案
    朝倉泉, 増原英彦, 青谷知幸
    日本ソフトウェア科学会第30回大会, 東京, 2013年 9月, ポスター発表




Author: Izumi Asakura

Created: 2017-06-12 月 02:18

Emacs 26.0.50 (Org mode 8.2.10)