Computational Logic Lab at JAIST

Contact

• Name: Tsubasa Takagi (Associate Professor)
• Affiliation: Japan Advanced Institute of Science and Technology (School of Information Science)
• E-mail:
• Room: I-54b (Information Science Research Bldg. 5F)
• Please email me first if you are interested in visiting/enrolling the lab/university (Online interview available.)

Rsearch Field

Our research field is theoretical computer science. In today's advanced IT society, everyone is using "computers" in the broad sense of the term, such as smartphones and personal computers, to enrich their lives. In our laboratory, we are not just using "computers" as tools, but are conducting research to theoretically re-formulate their mechanisms or to design new ones.

Specifically, we apply mathematical logic, a branch of mathematics, to scientifically explore the functions of programming and the specifications of software and communication protocols. Furthermore, we aim to realize highly reliable software by developing formal verification techniques that mathematically guarantee the correctness of algorithms and programs.

Keywords: Formal Specification/Verification, Many-sorted Equational Logic, Modal Logic, Dynamic Logic (Hoare Logic), Temporal Logic (Model Checking), Quantum Logic, Universal Algebra, State Transition System, Parallel Computation, Quantum Computation, Quantum Program/Protocol

Research Policy

• Basically, research discussion follows the flow of definition, theorem, and proof.
• However, the motivation is in computer science, not in mathematics.
• Implementation by programming may be done to demonstrate the validity of the theory.

Research Introduction

• Research Introduction
• Research Achievements
• Press Release

Student Guidance Policy

• I take into account as much as possible each student's background (what they studied in their undergraduate studies, their strengths and weaknesses, etc.) and motivation (what they want to research, what they want to learn, etc.).
• For students who do not have a theoretical background, I will guide you from the rudiments of mathematics.
• I value the spirit of independence, autonomy, and freedom, aiming to create an open laboratory.

Researchers develop and formulate new programming and specification description functions and mechanisms that have never been proposed by anyone before. In our laboratory, students can work on establishing and refining new theories that are application- and implementation-oriented (rather than just theory for theory's sake) after steadily acquiring basic knowledge of mathematics. The goal is to construct a sophisticated theory that can influence society one hundred years from now.

Beyond a certain level, engineers are required to have a high level of expertise. Specifically, they must not only be able to program and write specifications, but also have a rigorous understanding of their operating principles and functions using mathematics. In our laboratory, students can work on designing interpreters and compilers for imperative programming languages using functional programming languages, writing formal specifications based on type theory and universal algebra, and analyzing communication protocols and distributed systems (model checking).

School Life

• No mandatory events for students to attend other than weekly progress report meetings.
• Come to the lab any time you want, leave any time you want.
• If needed, I will hold study groups and laboratory camps to learn basic knowledge (free to attend).
• I will never force you to do research activities at a time when you are busy with job hunting, homecoming, etc.
• For students who want to learn more thoroughly, Long-term Study System is available.
• Can pay honorarium as Laboratory Assistant (LA) or RA (Research Assistant) if budget allows.
• All doctoral students who wish to be employed as UAs (University Assistants) will be paid an honorarium.
• If your application will be accepted by JSPS (JSPS Fellowship) or JAIST/JST (JAIST-SPRING Doctoral Fellow), you will be able to concentrate on your research under the support of living and research funds. See also the scholarship information.

Textbooks

Here are some textbooks that are relevant to our laboratory's research. Basically, you will read these textbooks (several of them) after being assigned to our laboratory. All of the textbooks are already distributed in our Lab or JAIST Library.

• Theorem Proving and Algebra (Joseph Goguen)
• Specification of Abstract Data Types (Jacques Loeckx, Hans-Dieter Ehrich, Markus Wolf)
• Foundations of Algebraic Specification and Formal Software Development (Donald Sannella, Andrzej Tarlecki)

• Algebraic Semantics of Imperative Programs (Joseph Goguen, Grant Malcolm)
• Designing Reliable Distributed Systems: A Formal Methods Approach Based on Executable Modeling in Maude (Peter Csaba Ölveczky)

Members

• Tsubasa Takagi (Associate Professor)
• Yang Song (Researcher)
• Shusuke Kobayashi (M1)
• Taiyo Nakamura (M1)
• Ryuichi Nagoshi (M1)
• Kai Yamaguchi (M1)