April 2022 – current: Research Associate
Department of Computer Science and 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 Computer Science and 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 graph rewriting languages 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
We propose to extend the concept of difference lists to general
data structures and call them difference data structures.
Difference lists are well-known in logic programming as a data
structure that realizes constant-time concatenation by retaining a
reference to the tail as well as the head of the list. In recent
years, they are also called list segments and appear as a typical
example of separa- tion logic, a logic for handling heaps and
pointers. Difference data structures can be utilized to discuss
various important concepts in programming languages including
functions, evaluation contexts, and continuations, in a unified
setting. To handle such structures succinctly and safely, we base
this work on a graph rewriting lan- guage. We propose a typing
method for graph rewriting languages based on graph grammar, which
covers structures beyond algebraic data types, to allow users to
define difference data types for two different major applications,
i.e., (i) users can describe powerful pat- tern matching with
user-defined shapes and (ii) the implementation can statically
type-check operations on difference data structures efficiently.
Our method introduces the concept of difference at the meta-level,
i.e., difference data types are automatically derived from the
base data type defined by graph grammar so that we can treat the
base structure and difference structure uniformly without type
conversion.
DOI:
10.1145/3678232.3678243
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
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. LMNtal programs
are guaranteed to be pointer-safe at the syntax level, but lack
the ability to statically report type errors, which can lead to
unintended behavior by the programmer. Since graph rewriting
languages can handle a broader class of graph structures than
algebraic data structures that can be handled by functional
languages, the formulation of types of graphs as the target of
computation is non-obvious. In particular, it is difficult to
develop a lightweight type-checking method for graph operations
that are described as rewriting from one subgraph to another. In
this paper, we propose a new static and lightweight type checking
method for graph rewriting languages based on difference of type
information.
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 (>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.
yamamoto <hidden-mark-you-know> ueda.info.waseda.ac.jpnyamamoto <hidden-mark-you-know> aoni.waseda.jp