山本直輝 - 上田研究室

各タイトルをクリックすると概要（と有る場合はPDF/DOIへのリンク）を展開します。

査読付き論文

Naoki Yamamoto, Kazunori Ueda: Engineering Grammar-based Type Checking for Graph Rewriting Languages.
In Proc. Twelfth International Workshop on Graph Computation Models (GCM 2021), 2021. (18 pages)

The ability to handle evolving graph structures is important both for programming languages and modeling languages. Of various languages that adopt graphs as primary data structures, a graph rewriting language LMNtal provides features and applications of both (concurrent) programming languages and modeling languages, and its implementation unifies ordinary program execution and model checking functionalities. Unlike pointer manipulation in imperative languages, LMNtal allows us to manipulate graph structures in such a way that the well-formedness of graphs is an invariant guaranteed by the language itself. However, since the shapes of graphs can be more complex and diverse than algebraic data structures such as lists and trees, it is important but not obvious to formulate types of graphs to verify individual programs. With this motivation, this paper discusses LMNtal ShapeType, a type checking method for rewrite rules that applies the basic idea of Structured Gamma to a concrete graph rewriting language. In this method, since types are defined as generative grammars written as LMNtal rules, type checking of LMNtal programs can be done by exploiting model checking features of LMNtal itself. We also gave a full implementation of type checking using the features of the LMNtal meta-interpreter.
PDF: Preproceedings or Our copy

Naoki Yamamoto, Kazunori Ueda: Engineering Grammar-based Type Checking for Graph Rewriting Languages.
In IEEE Access, Vol. 10, pp. 114612-114628, 2022. (17 pages)

The ability to handle evolving graph structures is important both for programming languages and modeling languages. Of various languages that adopt graphs as primary data structures, a graph rewriting language LMNtal provides features of both (concurrent) programming languages and modeling languages, and its implementation unifies ordinary program execution and model checking functionalities. Unlike pointer manipulation in imperative languages, LMNtal allows us to manipulate graph structures in such a way that the well-formedness of graphs is guaranteed by the language itself. However, since the shapes of graphs can be complex and diverse compared to algebraic data structures such as lists and trees, it is a non-obvious important task to formulate types of graphs to verify individual programs. With this motivation, this paper discusses LMNtal ShapeType, a type checking framework that applies the basic idea of Structured Gamma to a concrete graph rewriting language. Types are defined by generative grammars written as LMNtal rules, and type checking of LMNtal programs can accordingly be done by exploiting the model checking features of LMNtal itself. We gave a full implementation of type checking exploiting the features of the LMNtal meta-interpreter and confirmed that it works for practical operations on various graph structures, including single-step and multi-step operations on non-algebraic data structures and data structures with numerical shape constraints.
DOI: 10.1109/ACCESS.2022.3217913

Jin Sano, Naoki Yamamoto and Kazunori Ueda: Type Checking Data Structures More Complex Than Trees.
In Journal of Information Processing, Vol.31, pp. 112-130, 2023. (19 pages)

Graphs are a generalized concept that encompasses more complex data structures than trees, such as difference lists, doubly-linked lists, skip lists, and leaf-linked trees. Normally, these structures are handled with destructive assignments to heaps, which is opposed to a purely functional programming style and makes verification difficult. We propose a new purely functional language, λGT, that handles graphs as immutable, first-class data structures with a pattern matching mechanism based on Graph Transformation and developed a new type system, FGT, for the language. Our approach is in contrast with the analysis of pointer manipulation programs using separation logic, shape analysis, etc. in that (i) we do not consider destructive operations but pattern matchings over graphs provided by the new higher-level language that abstract pointers and heaps away and that (ii) we pursue what properties can be established automatically using a rather simple typing framework.
DOI: 10.2197/ipsjjip.31.112

Naoki Yamamoto, Kazunori Ueda: Grammar-based Pattern Matching and Type Checking for Difference Data Structures.
In Proc. 26th International Symposium on Principles and Practice of Declarative Programming (PPDP 2024), 2024. (13 pages)

We propose to extend the concept of difference lists to general data structures and call them difference data structures. Difference lists are well-known in logic programming as a data structure that realizes constant-time concatenation by retaining a reference to the tail as well as the head of the list. In recent years, they are also called list segments and appear as a typical example of separa- tion logic, a logic for handling heaps and pointers. Difference data structures can be utilized to discuss various important concepts in programming languages including functions, evaluation contexts, and continuations, in a unified setting. To handle such structures succinctly and safely, we base this work on a graph rewriting lan- guage. We propose a typing method for graph rewriting languages based on graph grammar, which covers structures beyond algebraic data types, to allow users to define difference data types for two different major applications, i.e., (i) users can describe powerful pat- tern matching with user-defined shapes and (ii) the implementation can statically type-check operations on difference data structures efficiently. Our method introduces the concept of difference at the meta-level, i.e., difference data types are automatically derived from the base data type defined by graph grammar so that we can treat the base structure and difference structure uniformly without type conversion.
DOI: 10.1145/3678232.3678243

査読なし論文

山本直輝, 上田和紀: グラフ書換え言語におけるグラフ操作の静的型検査.
In 日本ソフトウェア科学会第36回大会講演論文集 (JSSST 2019), 2019. (9 pages)

グラフ書換え言語 LMNtal は，グラフの書換えによって計算を表現するプログラミング言語としての側面と，一般の複雑なグラフ構造を扱えるモデリング言語としての側面を併せ持つ言語である．また，関数的アトムというデザインパターンを用いて，型の変換を伴う演算をも記述できる．一方で，グラフ書換え言語ではリストや二分木よりも複雑な構造を扱えるため，静的な型体系の定式化は自明でない．グラフ書換えの前後においてグラフの構造が保たれることを検査する静的型体系の先行研究として，Structured Gamma が存在する．そこで本研究では，Structured Gamma を基に，LMNtal に静的型を導入することを考える．本論文では，Structured Gamma の型検査手法を用いて，関数的アトムの入力と出力の型が整合していることを検査する手法を提案する．
PDF: 講演論文集

山本直輝, 上田和紀: グラフ書換え言語における数値制約を伴う型の静的型検査.
In 日本ソフトウェア科学会第37回大会講演論文集 (JSSST 2020), 2020. (12 pages)

グラフ書換え言語 LMNtal は，グラフの書換えによって計算を表現するプログラミング言語としての側面と，一般の複雑なグラフ構造を扱えるモデリング言語としての側面とを兼ね備えた言語である．そして，LMNtal の処理系は通常のプログラム実行とモデル検査の双方に対応した，強力な機能を提供している．グラフ書換え言語では，関数型言語で扱える代数的データ構造よりも広範な構造を扱えるため，静的な型検査の定式化は自明でない．そこで，書換え規則の型検査の手法として，グラフを対象とする静的型検査手法である Structured Gamma を基にした，LMNtalShapeType が提案されている．本論文では，LMNtal ShapeType に対し，LMNtal の拡張機能である型付きプロセス文脈を援用することにより，添字付きの非終端記号を表現し，赤黒木などの数値制約を伴うグラフ型を対象とした書換え規則の型検査を行う手法について述べる．
PDF: 講演論文集

山本直輝, 上田和紀: 定理証明支援系Coqによるグラフ書換え言語の性質証明.
In 日本ソフトウェア科学会第38回大会講演論文集 (JSSST 2021), 2021. (9 pages)

グラフ書換え言語 LMNtal は，グラフの書換えによって計算を表現するプログラミング言語としての側面と，一般の複雑なグラフ構造を扱えるモデリング言語としての側面とを兼ね備えた言語である．LMNtal プログラムは，読者の理解を助けるために，そのプログラムに対応するグラフの図的表現と併記されることがある．しかし，LMNtal の項はア・プリオリにグラフとして意味づけされているわけではなく，λ 計算や π 計算といった計算モデルと同様に，構文主導の意味論によって定義されている．そのため，LMNtal プログラムとその図的表現との対応関係は自明でない．そこで，LMNtal の項上の同値関係である構造合同関係と，グラフ理論におけるグラフ同型性との対応を明らかにするための準備として，本論文ではまず定理証明支援系 Coq の上で LMNtal の抽象構文と意味論を実装し，LMNtal 言語に関する性質の証明を Coq 上で行った．
PDF: 講演論文集

山本直輝, 上田和紀: データ構造としてのグラフを対象とした型の表現力拡張.
In 日本ソフトウェア科学会第39回大会講演論文集 (JSSST 2022), 2022. (16 pages)

グラフ書換え言語 LMNtal は，グラフの書換えによって計算を表現するプログラミング言語としての側面と，一般の複雑なグラフ構造を扱えるモデリング言語としての側面とを兼ね備えた言語である．グラフ書換え言語では，関数型言語で扱える代数的データ構造よりも広範な構造を扱えるため，計算対象となるグラフの型の定式化が課題となっている．そこで我々は，グラフの型に関する枠組みとして，形式文法に基づいた LMNtal ShapeType を提案し，文脈自由を超えた広範な型に対応した型検査手法を定式化してきた．しかし，ラムダ式のグラフによる表現やグリッドグラフなど，ルートの本数が一定でない型については，型の定義や検査手法が他の型に比べても自明でない．そこで本論文では，LMNtal ShapeType の定義および検査手法に対して拡張を施すことで，以上のようなグラフ型を対象とする型検査手法の定式化を目指す．
PDF: 講演論文集

山本直輝, 上田和紀: グラフ書換え言語におけるグラフ操作の軽量かつ静的な型検査.
In 日本ソフトウェア科学会第40回大会講演論文集 (JSSST 2023), 2023. (13 pages)

グラフ書換え言語 LMNtal は，グラフの書換えによって計算を表現するプログラミング言語としての側面と，一般の複雑なグラフ構造を扱えるモデリング言語としての側面とを兼ね備えた言語である．LMNtal プログラムは構文レベルでポインタ安全であることが保証されているが，静的に型エラーを報告する機能がないため，プログラマの意図しない振る舞いを起こす危険性がある．グラフ書換え言語では，関数型言語で扱える代数的データ構造よりも広範な構造を扱えるため，計算対象となるグラフの型の定式化は自明でない．特に，部分グラフから部分グラフへの書換えとして記述されるグラフの操作については，軽量な型安全性の検証手法が課題となっていた．そこで本論文では，グラフ書換え言語を対象とする静的かつ軽量な型検査手法として，型の差分情報に基づく手法を新たに提案する．
PDF: 講演論文集

ポスター発表

山本直輝, 上田和紀: 純粋型なし・型付きラムダ計算の実用的かつ高機能なインタプリタの実装.
In 日本ソフトウェア科学会第35回大会 (JSSST 2018), 2018.

Lambda*Magica をはじめ、ラムダ計算のインタプリタはこれまでにも幾つか存在した。しかし、Web ページ上で動作するといった実用性をもち、かつ簡約グラフを表示できる・マクロ定義ができるといった十分な機能性を備えたインタプリタは、著者の知る限り存在しない。そこで、これらの機能を備えた新たなインタプリタ「らむだフレンズ」を実装した。

山本直輝, 上田和紀: グラフ書換え言語における静的型体系LMNtal ShapeTypeの再定式化と拡張.
In 第21回プログラミングおよびプログラミング言語ワークショップ (PPL 2019), 2019.

グラフ書換え言語LMNtalは，一般のグラフ構造を容易に扱えるプログラミング言語である．しかし，LMNtalには型エラーを報告する機能がなく，プログラマの意図しない振る舞いを起こすことがある．そこで，LMNtalに静的型を導入することを考える．LMNtalを対象とする静的型体系の先行研究として，LMNtal ShapeTypeが存在する．本研究では，LMNtal ShapeTypeにおける既知の課題点を解決するにあたり，まずLMNtal ShapeTypeをより正確に定式化し，型検査の健全性・停止性の証明を与えた．また，型の表現力を高めるために基本型・複合型といった拡張機能を新たに導入した．

Naoki Yamamoto, Kazunori Ueda: Grammar-based Static Type Checking for Graph Rewriting.
In The 17th Asian Symposium on Programming Languages and Systems (APLAS 2019), 2019.

The ability to handle evolving graph structures is important both for programming languages and modeling languages. Of various languages that adopt graphs as primary data structures, a graph rewriting language LMNtal provides features and applications of both (concurrent) programming languages and modeling languages, and its implementation unifies ordinary program execution and model checking functionalities. Unlike pointer manipulation in imperative languages, LMNtal allows us to manipulate graph structures in such a way that the well-formedness of graphs is an invariant guaranteed by the language itself. However, since shapes of graphs can be more complex and diverse than algebraic data structures such as lists and trees, static type checking for describing and checking shapes of graphs handled by individual programs are highly useful. With this motivation, this paper discusses LMNtal ShapeType, a type checking framework that applies the basic idea of Shape Types to a concrete graph rewriting language. Features of LMNtal ShapeType include: (i) the type checking framework is formulated as a sublanguage of the host language and exploits the nondeterministic execution mechanism of LMNtal implementation straightforwardly for type checking; (ii) it is simple and yet can handle complex and diverse graph structures including skip lists, difference lists, red-black trees, lambda-graphs, and rectangular grids; (iii) constraints on shapes such as the balancing of trees can be handled within the framework; and (iv) the typing of functions, messages and data constructors can be handled within the framework in a uniform manner.

ようこそ！

職歴

2022年4月 – 現在: 助手

学歴

2021年4月 – 現在: 博士後期課程

2019年4月 – 2021年3月: 修士（工学）

2015年4月 – 2019年3月: 学士（工学）

研究分野

グラフ書換え言語のための型システム

証明支援系Coq上におけるグラフ書換え

ラムダ計算とグラフ

発表および文献