##### April 2022 – current: Research Associate

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

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 LanguagesLambda CalculusSet TheoryMathematical Logics
- Programming
TypeScriptC/C++JavaOCamlPythonVisual Basic (VBA)BASICFORTRAN
- Web Applications
TypeScriptHTML/CSS/JSNode.jsWebpack
- Music (esp. classical & choral)
T.RavenscroftJ.S.BachF.MendelssohnL.v.BeethovenLeroy Anderson
- Editing Books & Documents, Proofreading
Adobe CC (Indesign, Photoshop, Illustrator, After Effects)LaTeX/BeamerMicrosoft Office (Word, Excel, PowerPoint)

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

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

Supervisor: Professor Kazunori Ueda

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

Supervisor: Professor Kazunori Ueda

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

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.

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 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.

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

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

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

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

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

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

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

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

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.

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.

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.

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.

- 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