Welcome to my portfolio!

I'm full of curiosity about almost anything, whether it is related to Computer Science or not.

  • Discrete Mathematics
    Models of Computation (Automata, Turing Machines)
    Formal Languages
    Lambda Calculus
    Set Theory
    Mathematical Logics
  • Programming
    TypeScript
    C/C++
    Java
    OCaml
    Python
    Visual Basic (VBA)
    BASIC
    FORTRAN
  • Web Applications
    TypeScript
    HTML/CSS/JS
    Node.js
    Webpack
  • Music (esp. classical & choral)
    T.Ravenscroft
    J.S.Bach
    F.Mendelssohn
    L.v.Beethoven
    Leroy Anderson
  • Editing Books & Documents, Proofreading
    Adobe CC (Indesign, Photoshop, Illustrator, After Effects)
    LaTeX/Beamer
    Microsoft Office (Word, Excel, PowerPoint)

Work Experience

April 2022 – current: Research Associate

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

Education

April 2021 – current: Doctoral program

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

Supervisor: Professor Kazunori Ueda

April 2019 – March 2021: Master of Engineering

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

Supervisor: Professor Kazunori Ueda

April 2015 – March 2019: Bachelor of Engineering

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

Cumulative GPA: 3.57 / 4.00

Outstanding Student Award (Dean's Award, School of Fundamental Science and Engineering), March 2019

Research Topics

Type Systems for Graph Rewriting

The goal is to verify the type safety of rewrite rules targeting complicated graph structures rather than simple (algebraic) data structures (i.e., lists or trees). These are not typable with classic type systems in functional languages.

Graph Rewriting on Coq Proof Assistant

In the discussion on graph rewriting, there are many situations where subtle proofs are required. In particular, the arguments of the types above and the correspondence between structural congruences and graph isomorphisms need to be carefully discussed. Therefore, I aim to describe the syntax, semantics, and properties of LMNtal and prove them on the Coq Proof Assistant.

Lambda Calculus

Lambda calculus is highly well-known as the basis of functional languages. However, there are still many research areas that nobody has thoroughly explored before. For example, the following topics are actively researched even now: describing lambda terms as (hyper-)graphs and visualizing reduction graphs.

Presentations and Publications

Click each title to show its abstract (and PDF/DOI if available).

Refereed Papers

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

Unrefereed Papers

Naoki Yamamoto, Kazunori Ueda: Static type checking for graph manipulation in graph rewriting languages.
In Proc. The 36th JSSST Annual Conference (JSSST 2019), 2019. (in Japanese, 9 pages)

A graph rewriting language LMNtal has aspects of both a programming language which expresses calculation by graph rewriting and a modeling language which can handle complicated graph structures. Also, we can use a design pattern called functional atoms in order to describe calculations with type transformation. On the other hand, since graph rewriting languages can handle a broader class of graph structures than lists or trees, formulation of static type system for those languages is not obvious. Structured Gamma is known as a static type system which verifies that graph structures will not be destroyed by graph rewriting. Therefore we shall introduce a static type system based on Structured Gamma for LMNtal. This paper proposes a type checking method for calculations with type transformation, using the type checking algorithm in Structured Gamma.
PDF: Proceedings

Naoki Yamamoto, Kazunori Ueda: Static Type Checking for Types with Numeric Constraints in Graph Rewriting Languages.
In Proc. The 37th JSSST Annual Conference (JSSST 2020), 2020. (in Japanese, 12 pages)

A graph rewriting language LMNtal has aspects of both a programming language that expresses computation by graph rewriting and a modeling language that can handle complicated graph structures. Furthermore, its implementation integrates both regular program execution and model checking. In graph rewriting languages, we can handle a broader class of graph structures than algebraic data structures that can be handled by functional languages. As a type checking method for rewrite rules, LMNtal ShapeType was proposed based on Structured Gamma, a static type checking method for graphs. This paper proposes a type checking method for rewrite rules targeting graph types with numeric constraints (e.g., red-black trees) by using typed process context, which is an extension of LMNtal, as the index of nonterminal symbols.
PDF: Proceedings

Naoki Yamamoto, Kazunori Ueda: Proving Properties of Graph Rewriting Languages with the Coq Proof Assistant.
In Proc. The 38th JSSST Annual Conference (JSSST 2021), 2021. (in Japanese, 9 pages)

A graph rewriting language LMNtal has aspects of both a programming language that expresses computation by graph rewriting and a modeling language that can handle complicated graph structures. LMNtal programs are sometimes accompanied by a graphical representation of the corresponding graph to aid readers' understanding. However, LMNtal terms are not semantically defined as graphs a-priori, but are defined by syntax-directed semantics, similar to computational models like the λ-calculus and π-calculus. Therefore, the correspondence between LMNtal programs and their graphical representations is not obvious. In preparation for clarifying the correspondence between the structural congruence, which is an equivalence relation among LMNtal terms, and graph isomorphism in graph theory, this paper first implements the abstract syntax and semantics of LMNtal on the Coq proof assistant, and then proves some properties of the LMNtal language on Coq.
PDF: Proceedings

Naoki Yamamoto, Kazunori Ueda: Extending the Expression Power of Types for Graphs as a Data Structure.
In Proc. The 39th JSSST Annual Conference (JSSST 2022), 2022. (in Japanese, 16 pages)

A graph rewriting language LMNtal has aspects of both a programming language that expresses computation by graph rewriting and a modeling language that can handle complicated graph structures. In graph rewriting languages, we can handle a broader class of graph structures than algebraic data structures that can be handled by functional languages. We have proposed LMNtal ShapeType based on formal grammars as a framework for graph types and formulated a type checking method for broader classes of types beyond context-free types. However, for types with an unbounded number of roots, such as lambda graphs and grid graphs, the type definition and checking methods are not so obvious. This paper aims to formulate a type checking method for the above graph types by extending the definition of LMNtal ShapeType.
PDF: Proceedings

Posters

Naoki Yamamoto, Kazunori Ueda: Implementation of an interpreter for pure untyped and typed lambda calculus.
In Proc. The 35th JSSST Annual Conference (JSSST 2018), 2018. (in Japanese)

There are several interpreters for lambda calculus including Lambda*Magica. However, none of them has both usability (e.g., running on Web pages) and enough functionality (e.g., visualizing reduction graphs or defining macros). Then we implemented the new interpreter, named Lambda Friends, equipped with these features.

Naoki Yamamoto, Kazunori Ueda: Reformulation and extension of LMNtal ShapeType, a static type system for graph rewriting language.
In Proc. The 21st JSSST Workshop on Programming and Programming Languages (PPL 2019), 2019. (in Japanese)

LMNtal is a graph rewriting programming language, with which we can easily handle general graph structures. However, LMNtal programs may cause unexpected behavior since LMNtal has no features to report type errors. Then we should introduce static typing to LMNtal. LMNtal ShapeType is an existing research of static type system targeting LMNtal. In this research, we precisely reformulated LMNtal ShapeType and gave proofs for soundness and termination of the type checking before we solve known issues in LMNtal ShapeType. Then we introduced extensions such as basic types and compound types to improve the expressive power of the types.

Naoki Yamamoto, Kazunori Ueda: Grammar-based Static Type Checking for Graph Rewriting.
In Proc. 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.

Software

Lambda Friends

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

Other Skills & Activities

  • Fluent in Japanese, conversational English
  • Acted Bass part leader (2017) and vice president (2018) of Waseda University Mixed Chorus
  • Performed Teaching Assistant (TA) for over 10 lectures (2018–) at the university
  • TOEIC Listening & Reading Test Score: 795 / 990, December 2017
  • Applied Information Technology Engineer Examination (AP), April 2018
  • Member of Waseda Chapter (Mu-Tau) of IEEE-HKN (Eta-Kappa-Nu, international honor society) since August 2019

Contact

yamamoto <hidden-mark-you-know> ueda.info.waseda.ac.jp