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