Information Systems Architecture Science Research Division

Information Systems Architecture Science Research Division Assistant Professor
Research Fields: Software Infrastructure

Introduction of research by science writer

Aiming for bug-free software

Programming language theory is a discipline that researches the semantics and structures of programming languages (Fortran, COBOL, C, Python, etc.). We do not directly implement software useful for business or society, but research on how to write correct software free of bugs (defects) could have a large impact in today's society where software occupies an important position.

Elimination of software bugs is a major issue, but the reality is that it is quite difficult. Research in the field of programming language theory is carried out using mathematical tools, but defining a bug and defining how a program should work are difficult tasks, and even if they are successfully defined, verifying whether the program works correctly according to the given specifications is even more difficult.

Software bug detection method

One method of detecting bugs in programs is a type system, which assigns various types to expressions and examines whether values are used correctly. My research so far has been on a verification system that combines dynamic typing*1 and static typing*2 to detect program bugs as far as possible, while being simple and quick to use.

Dynamic typing allows types to be checked while the program is running, making flexible programming possible (aimed at prototype implementation); in contrast, static typing checks types before the program is executed so that errors do not occur during execution, which is suited to large-scale system development. I am developing a verification system that combines these two typing methods so that it possesses the advantages of both.

*1 A method of verifying whether a program is operating correctly using actual values during program execution, without assigning types to values such as program variables, subroutine arguments, or return values in advance.

*2 A method of verifying and guaranteeing that functions will only process data of the correct type that matches the format before running the program.

Programming language theory research using machine learning

In the future, I would like to try to design/develop a "programming language for machine learning" that incorporates probability and statistics to enable efficient machine learning. I am also interested in "machine learning for programming languages," aimed at guaranteeing the safety of programs, and I would like to do research on using machine learning to carry out reliable and efficient bug bashing.

Neither of these is easy, but I want to tackle them seriously and continue research aimed ultimately at automatic bug bashing using machine learning and automation of programming itself.

Interview/text by Tsutomu Sahara



Reading "Types and Programming Languages," an introductory book on type systems that a friend recommended to me in my third year of university, was what made me want to become a researcher in programming language theory. The book revealed to me just how interesting programming language theory is. If I had not encountered that book, I might not have my current life as a researcher. I hope to continue to explore the things that interest me.

PDF Download