Tsubasa Takagi's Personal Webpage

Tsubasa Takagi ORCID logo 0000-0001-9890-1015

Contact

Research History

Work Experience

Education

Research Interests

I am working on the formal verification infrastructure for quantum computer programs (quantum programs).

Since quantum computation is based on a completely different principle from classical computation, new formal verification techniques for quantum programs are required to verify whether a quantum program satisfies specifications.

I am aiming to establish formal verification techniques for quantum programs by combining modal logics (dynamic logic and temporal logic), which have been used for formal verification of classical computation, with quantum logic.

Area of Study

Keywords

Quantum Logic, Quantum Computation, Formal Verification, Modal Logic, Dynamic Logic, Temporal Logic, Equational Logic, Algebraic Structure, State Transition System, Model Checking, Automata

Publications

Journal Papers

  1. Tsubasa Takagi, Semantic Analysis of a Linear Temporal Extension of Quantum Logic and Its Dynamic Aspect, ACM Transactions on Computational Logic, forthcoming, ACM, 2022. [PDF]
  2. Tsubasa Takagi, Translation from Three-Valued Quantum Logic to Modal Logic, International Journal of Theoretical Physics, 60(1): 366–377, Springer, 2021. [PDF]
  3. Tsubasa Takagi, Observable-Dependent Kripke Semantics for Quantum Logic (in Japanese), Japanese Student Research Notes of Philosophy of Science, 4: 1-8, Japan Association for Philosophy of Science, 2021. (Japanese Title: 量子論理のオブザーバブル依存Kripke意味論, 新進研究者 Research Notes, 4: 1-8, 科学基礎論学会, 2021.) [PDF]

Conference Papers

  1. 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 (FAVPQC 2022), CEUR Workshop Proceedings, 3280: 2-15, 2022. [PDF]

Research Grants

  1. Construction of Mathematical Logic System to Verify Quantum Communication Networks and Its Quantum Computational Implications (Japanese Title: 量子通信ネットワークを検証する数理論理体系の構築と量子計算的意味付け), Grant-in-Aid for JSPS Research Fellow Grant Number 22J23575 (April. 2022 -- March. 2025)

Teaching

Financial Support

  1. JSPS Research Fellow (DC1), Japan Society for the Promotion of Science (April. 2022 -- March. 2025)
  2. Research Assistant in Ogata Laboratory at Japan Advanced Institute of Science and Technology (October. 2021 -- March. 2022)
  3. JASSO Scholarship for Ph.D. Students, Exemption from refund due to outstanding performance, Japan Student Services Organization (October. 2021 -- March. 2022)
  4. JASSO Scholarship for Master's Students, Exemption from refund due to outstanding performance, Japan Student Services Organization (April. 2020 -- September. 2021)
  5. SD Program Scholarship, Japan Advanced Institute of Science and Technology (April. 2020 -- March. 2022)