Updated on 2025/01/04

写真a

 
YAMAMOTO, Naoki
 
Affiliation
Faculty of Science and Engineering, School of Fundamental Science and Engineering
Job title
Research Associate

Research Experience

  • 2022.04
    -
    Now

    Waseda University   School of Fundamental Science and Engineering   Research Associate

Education Background

  • 2021.04
    -
    Now

    Waseda University   Graduate School of Fundamental Science and Engineering   Department of Computer Science and Communications Engineering  

    Ueda Laboratory

  • 2019.04
    -
    2021.03

    Waseda University   Graduate School of Fundamental Science and Engineering   Department of Computer Science and Communications Engineering  

    Ueda Laboratory

  • 2015.04
    -
    2019.03

    Waseda University   School of Fundamental Science and Engineering   Department of Computer Science and Engineering  

    Ueda Laboratory (since April 2018)

Research Areas

  • Software   Programming Languages

Research Interests

  • Graph Pattern Matching

  • Static Type Checking

  • Graph Rewriting Languages

Awards

  • Outstanding Student Award (Dean's Award)

    2019.03   Waseda University  

    Winner: Naoki Yamamoto

 

Papers

▼display all

Works

  • Lambda Friends, a web interpreter for the lambda calculus

    Naoki Yamamoto  Web Service 

    2018.01
    -
    Now

     View Summary

    Lambda Friends is a web-based interpreter for untyped & simply typed lambda calculus. It's written in TypeScript (>5k Lines of Code), published as Open Source Software, and used for education in a required course on Programming Languages (>100 students) in the Department of Computer Science and Engineering, Waseda University.

Research Projects

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

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

    Project Year :

    2023.04
    -
    2026.03
     

    上田 和紀, 山本 直輝

 

Internal Special Research Projects

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

    2023   上田和紀

     View Summary

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

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

    2022   上田和紀

     View Summary

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