ソフトウェアを科学する
信頼性が高く効率も良いソフトウェアを構築するために必要な計算の理論とその情報システムへの応用の研究を行っています。特に最先端の関数型プログラミングの理論と技術を基軸としたソフトウェア理論を研究してきました。「計算」がもつ基本的な性質を解明する基礎研究と、それを元にしたソフトウェア検証、データベースといった情報システムのための推論・実装技術への応用研究を行っています。理論研究では、λ計算や項書換え系を基本とする計算モデルの基礎理論、論理学や型理論を基本とするプログラム理論、普遍代数学や圏論の数学的構造を用いたプログラム意味論、といった様々な計算理論を横断的に統合した数理的手法でソフトウェア理論の研究を展開しています。下記のようなテーマについて研究を行っています。
- 高階書換え系の代数モデルと停止性、合流性自動検証ツール [PACMPL17]
- グラフ型データベースの新しい基礎理論 [MSCS18]
- 依存型による安全なデータ構造とその関数型プログラミング [LMCS17]
- 多相型代数理論による関数型プログラミング言語のメタ理論
情報学部
准教授 浜名 誠
- [MSCS18] The Algebra of Recursive Graph Transformation Language UnCAL: Complete Axiomatisation and Iteration Categorical Semantics, x(with Kazutaka Matsuda and Kazuyuki Asada), Mathematical Structures in Computer Science, Volume 28, Issue 2, pp.287-337, Cambridge University Press, doi:10.1017/S096012951600027X, 2018.
- [PACMPL17] How to Prove Your Calculus is Decidable: Practical Applications of Second-order Algebraic Theories and Computation, Proceedings of ACM on Programming Languages, Vol. 1, Issue ICFP, Article No. 22, pp.1-28, ACM Press, doi:10.1145/3110266, 2017.
- [LMCS17] Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories, Logical Methods in Computer Science, Vol. 13, No.3, pp.1-38, doi:10.23638/LMCS-13(4:8)2017, 2017.