2024/03/28 更新

写真a

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

経歴

  • 2022年04月
    -
    継続中

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

 

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

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

    2022年   上田和紀

     概要を見る

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