2025/01/03 更新

写真a

ヤマモト ナオキ
山本 直輝
所属
理工学術院 基幹理工学部
職名
助手

経歴

  • 2022年04月
    -
    継続中

    早稲田大学   基幹理工学部   助手

学歴

  • 2021年04月
    -
    継続中

    早稲田大学   大学院基幹理工学研究科   情報理工・情報通信専攻 博士後期課程  

    上田研究室

  • 2019年04月
    -
    2021年03月

    早稲田大学   大学院基幹理工学研究科   情報理工・情報通信専攻 修士課程  

    上田研究室

  • 2015年04月
    -
    2019年03月

    早稲田大学   基幹理工学部   情報理工学科  

    上田研究室 (2018年4月より配属)

研究分野

  • ソフトウェア   プログラミング言語

研究キーワード

  • グラフパターンマッチ

  • 静的型検査

  • グラフ書換え言語

受賞

  • 基幹理工学部長賞 優秀賞

    2019年03月   早稲田大学  

    受賞者: 山本直輝

 

論文

▼全件表示

Works(作品等)

  • Webブラウザ上で動作するラムダ計算インタプリタ「らむだフレンズ」

    山本直輝  Web Service 

    2018年01月
    -
    継続中

     概要を見る

    Web上で動作する型なし・型付きラムダ計算のインタプリタ。 TypeScript (5,000 LOC超) で書かれており、OSSとして公開されている。 早稲田大学情報理工学科において100名超が受講する必修科目である 「プログラミング言語」にて2018年度より継続して使用されている。

共同研究・競争的資金等の研究課題

  • 強力なデータ構造と並行性をもつ高水準言語の解析・実装技法の多面的開拓

    日本学術振興会  科学研究費助成事業

    研究期間:

    2023年04月
    -
    2026年03月
     

    上田 和紀, 山本 直輝

 

特定課題制度(学内資金)

  • 形式文法に基づいたデータ構造のパターンを応用したプログラム実行と検証

    2023年   上田和紀

     概要を見る

    一般のグラフ構造は,代数的データ型(リストや木構造)よりも複雑な構造をもち,それ故に既存のプログラミング言語では安全かつ簡潔な表現が困難である.例えば,C言語のようなポインタを扱える言語であれば,ポインタの接続構造としてグラフを表現することができるが,依然として不正なポインタが発生する危険性がある.そこで,グラフを第一級オブジェクトとしてもち,それを書き換えることによって計算を表現する,グラフ書換え言語というパラダイムが提案されている.中でもLMNtalは,アトム(ノード)やルール(書換え規則)といった最小限の言語要素からなる言語である.LMNtalプログラムはwell-formedであるかぎり,不正なポインタを含まない.この意味で,LMNtalは言語仕様のレベルで不正なポインタを排除しており,ポインタ安全といえる.一方で,LMNtalには静的型の概念がないため,書換えの結果がプログラマの意図しないものとなることがある.グラフ書換え言語では,関数型言語で扱える代数的データ構造よりも広範な構造を扱えるため,計算対象となるグラフの型の定式化は自明でない.そこで我々は,グラフ文法に基づく型定義手法を提案し,ユーザー定義のグラフ型を用いてパターンマッチを記述できる拡張機能を導入することで書換え規則の表現力を向上するとともに,書換え規則の静的型検査手法を確立することを目的としている.2023年度は,まず局所的な接続関係の整合性に着目した型検査手法であるLMNtypeの定式化を行うとともに,既存の拡張言語であるCSLMNtalとの技術交流を行った.また,グラフ文法に基づくグラフ型検査にtoken passingの手法を用いることにより最適化する研究にも参画した.

  • 定理証明支援系によるグラフ書換え言語の形式化

    2022年   上田和紀

     概要を見る

    グラフ書換え言語LMNtalは,複雑な接続構造とその安全な操作を簡潔に表現できる言語である.LMNtalの項は,そのプログラムに対応するグラフの図的表現と併記されることがあるが,グラフ理論ではなく,構文主導の意味論に基づいて定義されている.そのため,LMNtalの項とその図的表現との対応関係,特にLMNtal項上の構造合同関係と,図的表現の間のグラフ同型との対応関係は非自明な課題である.本研究では,まず証明対象となるデータ構造の定義と,証明の大まかな方針を定めた.また,その知見を活かし,データ構造としてハイパーグラフを採用し形式文法に基づいた型定義を行う関数型言語λGTの提案に参画した.