浅井 健一

ASAI Kenichi

職名

准教授

所属

基幹研究院 自然科学系

人間文化創成科学研究科 博士後期課程 理学専攻

人間文化創成科学研究科 博士前期課程 理学専攻

理学部 情報科学科

主担当学科

理学部情報科学科

担当大学院(博士前期課程)

人間文化創成科学研究科理学専攻情報科学コース

担当大学院(博士後期課程)

人間文化創成科学研究科理学専攻情報科学領域

URL

写真a

研究キーワード 【 表示 / 非表示

  • 部分継続、部分評価、自己反映言語

研究内容 【 表示 / 非表示

  • プログラミング言語に置ける部分継続の基礎理論の確立とその応用の開拓を行うと同時に、型の入った効率的な処理系の作成を目指す。具体的には、基礎理論として (1) 型システムの基本的な性質の確立、および (2) 継続計算の処理系作成のための基礎技術の確立を目指す。また、継続計算用型システムの応用として (3) 例外解析の定式化を行う。さらに (4) これらの知見をあわせ処理系の実装を行う。

教育内容 【 表示 / 非表示

  • 「データ構造とアルゴリズム」でデータ構造の初歩を、「関数型言語」でプログラムの基本的な考え方を、「言語理論とオートマトン」で言語処理系の基礎を、「コンパイラ構成論」でコンパイラの中身について学ぶ。

将来の研究計画・研究の展望・共同研究の可能性 【 表示 / 非表示

  • MetaOCaml などの段階的計算体系に束縛時解析を導入して、自己反映言語のコンパイルを実現する。

受験生等へのメッセージ 【 表示 / 非表示

  • 情報科学の基礎理論の分野で確かな一歩を一緒に踏み出しましょう。

学位 【 表示 / 非表示

  • 博士(理学), 1994年08月

学内職務経歴 【 表示 / 非表示

  • 人間文化創成科学研究科 研究院【基幹部門】 自然・応用科学系,准教授

  • 基幹研究院 自然科学系,准教授

  • 人間文化創成科学研究科 教育院【博士後期課程】 理学専攻,准教授

  • 人間文化創成科学研究科 博士後期課程 理学専攻,准教授

  • 人間文化創成科学研究科 教育院【博士前期課程】 理学専攻,准教授

全件表示 >>

 

学術著書・訳書 【 表示 / 非表示

  • プログラミングの基礎

    サイエンス社, 2007年02月, 浅井 健一, 教科書

  • Trends in Functional Programming

    Logical Relations for Call-by-value Delimited Continuations, Intellect, 2007年07月, Asai, K., Marko van Eekelen, 研究書, 63-78

論文 【 表示 / 非表示

  • Report on a User Test and Extension of a Type Debugger for Novice Programmers

    Electronic Proceedings in Theoretical Computer Science, 170巻(頁1 - 18), 2014年12月, Ishii, Y., and K. Asai, 原著, 研究論文(学術雑誌), 共著者

  • 重み付き型エラースライスの提案

    コンピュータソフトウェア, 31巻4号(頁131 - 148), 2014年11月, 対馬 かなえ、浅井 健一, 原著, 研究論文(学術雑誌), 共著者

  • Formalizing a Correctness Property of a Type-Directed Partial Evaluator

    Programming Languages meets Program Verification (PLPV)(頁41 - 46), 2014年01月, Hirota, N., and K. Asai, 原著, 研究論文(国際会議プロシーディングス), 共著者

  • 限定継続命令 shift/reset 付き型主導部分評価器の抽出

    情報処理学会論文誌 プログラミング (PRO), 6巻4号(頁50 - 64), 2013年12月, 廣田 知子、浅井 健一, 原著, 研究論文(学術雑誌), 共著者

  • shift/reset によるモナドトランスフォーマの提案と実装

    第15回プログラミングおよびプログラミング言語ワークショップ, 2013年03月, 金子 ちひろ、浅井 健一, 原著, 研究論文(学術雑誌), 共著者

全件表示 >>

研究発表 【 表示 / 非表示

  • 型エラースライシングを利用した型エラーデバッガに関する実装と考察

    脇川奈穂、対馬かなえ、浅井健一, 国内, 2017年03月, 第19回プログラミングおよびプログラミング言語ワークショップ, 山梨県笛吹市, 日本ソフトウェア科学会, 一般発表, 共著者

  • ジェネリックプログラミングを用いた証明木GUIライブラリの実装

    松本晴香、浅井健一, 国内, 2017年03月, 第19回プログラミングおよびプログラミング言語ワークショップ, 山梨県笛吹市, 日本ソフトウェア科学会, 一般発表, 共著者

  • Agda によるダイクストラのアルゴリズムの証明

    山田麗、浅井健一, 国内, 2017年03月, 第19回プログラミングおよびプログラミング言語ワークショップ, 山梨県笛吹市, 日本ソフトウェア科学会, 一般発表, 共著者

  • 型エラースライシングを利用した型エラーデバッガに関する実装と考察

    脇川奈穂、対馬かなえ、浅井健一, 国内, 2017年01月, 第58回プログラミング・シンポジウム, 静岡県伊東市, 情報処理学会, 一般発表, 共著者

  • 強い型付けを利用したプログラミング初学者のための開発環境

    石井柚季、浅井健一, 国内, 2016年03月, 第18回プログラミングおよびプログラミング言語ワークショップ, 岡山県玉野市, 日本ソフトウェア科学会, 一般発表, 共著者

全件表示 >>

研究活動に対する受賞 【 表示 / 非表示

  • 第20回研究論文賞

    日本ソフトウェア科学会, 対馬 かなえ、浅井 健一, 重み付き型エラースライスの提案, 2016年09月, 国内

  • Peter Landin Prize

    Implementation and Application of Functional Languages, IFL, Kanae Tsushima, Kenichi Asai, An Embedded Type Debugger, 2013年03月, 国外

  • 論文賞

    第12回プログラミングおよびプログラミング言語ワークショップ プログラム委員会, 木谷 有沙、浅井 健一, プログラム変換によるインタプリタからのコンパイラの導出, 2010年03月, 国内

外部資金等受入(教育・社会貢献の外部資金を含む) 【 表示 / 非表示

  • プログラム意味論に基づく先進的なプログラミング環境の構築

    基盤研究(C), 浅井 健一, 2017年度, 1,100千円

  • プログラム意味論に基づく先進的なプログラミング環境の構築

    基盤研究(C), 浅井 健一, 2016年度, 1,200千円

  • プログラム意味論に基づく先進的なプログラミング環境の構築

    基盤研究(C), 浅井 健一, 2015年度, 1,300千円

  • 自己反映言語の効率的実装とそれを支える基盤技術

    基盤研究(C), 2014年度, 600千円

  • 自己反映言語の効率的実装とそれを支える基盤技術

    基盤研究(C), 2013年度, 800千円

全件表示 >>

 

学術団体の役員、委員等としての貢献 【 表示 / 非表示

  • Higher-Order and Symbolic Computation (Springer), 委員,2012年09月 - 現在, 1388-3690, 国外

  • Journal of Functional Programming (Cambridge University Press), 委員,2012年09月 - 2013年10月, 0956-7968, 国外