Building Theoretical Foundation of Computer Science

TAKAGI Laboratory
Associate Professor：TAKAGI Tsubasa

E-mail：
［Research areas］
Theoretical Computer Science
［Keywords］
Many-sorted Equational Logic, Modal Logic, Dynamic Logic (Hoare Logic), Temporal Logic (Model Checking), Quantum Logic

Skills and background we are looking for in prospective students

It is recommended that students have a motivation to not only use the computer as a tool, but also to understand (or invent) the mechanism of computers.

What you can expect to learn in this laboratory

In this laboratory, students will acquire the ability to solve social problems based on solid logical/mathematical thinking skills. These abilities are versatile and highly applicable to any job after completion of the program.

【Job category of graduates】IT and communication companies, research institutes

Research outline

One important theoretical foundation of computer science can be found in mathematical logic. Mathematical logic was born before the birth of computers and has been deeply involved in the birth and development of computers. In this laboratory, we are studying rigorous proofs of the correctness of quantum computation (quantum protocols and quantum programs) using mathematical logic.

To improve reliability of quantum computation, in which conventional intuition does not work well, it is important to provide a mathematical proof (formal verification) that the design of quantum computation is correct.

On the other hand, formal verification of classical computation has a long history. It has been found that mathematical logics such as many-sorted equational logic and modal logic (dynamic logic and temporal logic) are effective for this purpose. Therefore, we conduct formal verification of quantum computation by improving or extending these mathematical logics.

1. Formal Verification of Quantum Computation Based on Many-sorted Equational Logic

To conduct formal verification, a mathematically rigorous specification of a system or program is first required. In particular, many-sorted equational logic provides the theoretical basis for rigorous specifications expressed by equations (called algebraic specifications), and then formal verification is conducted by equational reasoning based on these specifications. This method has been used with great success in formal verification of classical computation.

Therefore, it is a natural idea to follow this approach and give an algebraic specification of a quantum computation based on many-sorted equational logic. In addition to this, we have successfully implemented an algebraic specification of quantum computation on a classical computer for automated formal verification.

2. Formal Verification of Quantum Computation Based on Dynamic Quantum Logic

It is also interesting to start from the research question of what is the logic of quantum computation, rather than from classical formal verification. John von Neumann, the father of the computer, and his colleague created quantum logic as the logic of quantum mechanics in 1936. Since quantum computation was born half a century later, quantum logic and quantum computation were unrelated at that time. So, how can quantum logic be reborn as a modern logic by incorporating the viewpoint of quantum computation?

One answer to this question is dynamic quantum logic, which integrates dynamic logic and quantum logic. In our research, by formulating an algebra of dynamical quantum logic, we have succeeded in formally verifying various quantum programs based on it in a manner similar to that of Hoare logic. Dynamic quantum logic is also interesting as a merely mathematical structure, and the investigation of its properties is useful for understanding of quantum computation.

Key publications

1. Tsubasa Takagi, Semantic Analysis of a Linear Temporal Extension of Quantum Logic and Its Dynamic Aspect. ACM Transactions on Computational Logic, 24(3): 1-21, ACM, 2023.
2. Tsubasa Takagi, Canh Minh Do, Kazuhiro Ogata, Automated Quantum Program Verification in Dynamic Quantum Logic. In Proceedings of DaLí: Dynamic Logic – New Trends and Applications, Lecture Notes in Computer Science (LNCS), 14401: 68- 84, 2024.
3. Tsubasa Takagi, An Algebra of Quantum Programs with the Kleene Star Operator. In Proceedings of International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols, CEUR Workshop Proceedings, 3280: 2-15, 2022.