Updated on 2024/07/28

Information

 

写真a

 
GAINA MIRCEA DANIEL
 
Organization
Institute of Mathematics for Industry Associate Professor
School of Sciences Department of Mathematics（Joint Appointment）
Graduate School of Mathematics Department of Mathematics（Joint Appointment）
Joint Graduate School of Mathematics for Innovation （Joint Appointment）
Title
Associate Professor
Contact information
メールアドレス
Tel
0928024425
Profile
My research is focused on algebraic specification, one of the most promising aproach to formal methods assisting the developing of software systems at several stages such as design, specification and formal verification. Algebraic specification and programming languages are rigorously based on logic, which amounts to the existence of a logical system underlying the language such that each language feature and construction can be expressed as a mathematical entity of the underlying logic.
Homepage
External link

Degree

  • BSc in informatics from University of Bucharest

  • Master's degree in fundamentals of informatics from University of Bucharest

  • Master's degree in algebraic specification from Normal Superior School of Bucharest

  • PhD in information science from Japan Advanced Institute of Science and Technology

Research History

  • October 2004 - October 2006: research assistant at University of Bucharest October 2009 - July 2010: postdoctoral researcher at Japan Advanced Institute of Science and Technology August 2010 - March 2013: research assistant professor at Japan Advanced Institute of Science and Technology April 2013 - March 2017: assistant professor at Japan Advanced Institute of Science and Technology April 2017 - March 2022: assistant professor at Kyushu University April 2022 - present: associate professor at Kyushu University

Research Interests・Research Keywords

  • Research theme：Reconfigurable systems are found everywhere: software-driven medical devices (such as infusion pumps, pacemakers, imaging machines and pill cameras), intelligent transportation systems, cars, or mobile robots. They all interact with their users and the environment in which they operate. Reconfigurable systems are often used in safety-critical areas where any malfunction may cause serious injuries to human beings. The safety requirements can be fulfilled only by applying formal methods. The objective is to develop a software tool for the formal specification and verification of reconfigurable systems.

    Keyword：theorem proving, reconfiguration paradigm, hybrid systems, verification methodology

    Research period： 2023.4 - 2026.4

  • Research theme：Recent developments of computer systems have triggered a paradigm shift from standard applications with fixed resources to reconfigurable systems, i.e. applications that work in different operation modes, called configurations, and react flexibly to internal and external stimuli for optimizing their performance. Very often the operation of reconfigurable systems is safety-critical: any malfunction may result in the serious injury to people. The safety requirements can be fulfilled only by applying formal methods. The purpose is to provide a solid logic-based foundation for developing a formal method to describe reconfigurable systems and to reason formally about their properties.

    Keyword：reconfigurable systems, formal methods, hybrid-dynamic logics

    Research period： 2020.4 - 2023.4

Papers

  • Forcing and Calculi for Hybrid Logics Reviewed International journal

    Journal of the Association for Computing Machinery   67 ( 4 )   1 - 55   2020.6

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    DOI： https://doi.org/10.1145/3400294

    Other Link： https://dl.acm.org/doi/10.1145/3400294

    Repository Public URL： https://hdl.handle.net/2324/7172111

  • Forcing, Transition Algebras, and Calculi Reviewed International journal

    51st EATCS International Colloquium on Automata, Languages and Programming, ICALP 2024   2024.5

    　More details

    Language：English   Publishing type：Research paper (international conference proceedings)  

  • Omitting Types Theorem in hybrid dynamic first-order logic with rigid symbols Reviewed International journal

    Annals of Pure and Applied Logic   174 ( 3 )   2023.3

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    DOI： https://doi.org/10.1016/j.apal.2022.103212

  • Robinson consistency in many-sorted hybrid first-order logics Reviewed International journal

    Advances in Modal Logic 2022, AiML 2022, Rennes, August 22-25   2022.8

    　More details

    Language：English   Publishing type：Research paper (international conference proceedings)  

  • Lindström’s theorem, both syntax and semantics free Reviewed International journal

    Daniel Găină, Tomasz Kowalski

    32 ( 5 )   942 - 975   2022.7

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    Lindström’s theorem characterizes first-order logic in terms of its essential model theoretic properties. One cannot gain expressive power extending first-order logic without losing at least one of compactness or downward Löwenheim–Skolem property. We cast this result in an abstract framework of institution theory, which does not assume any internal structure either for sentences or for models, so it is more general than the notion of abstract logic usually used in proofs of Lindström’s theorem; indeed, it can be said that institutional model theory is both syntax and semantics free. Our approach takes advantage of the methods of institutional model theory to provide a structured proof of Lindström’s theorem at a level of abstraction applicable to any logical system that is strong enough to describe its own concept of isomorphism and its own concept of elementary equivalence. We apply our results to some logical systems formalized as institutions and widely used in computer science practice.

    DOI： https://doi.org/10.1093/logcom/exab073

  • Fraïssé-Hintikka Theorem in institutions Reviewed International journal

    Daniel Găină, Tomasz Kowalski

    30 ( 7 )   1377 - 1399   2020.10

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    We generalize the characterization of elementary equivalence by Ehrenfeucht–Fraïssé games to arbitrary institutions whose sentences are finitary. These include many-sorted first-order logic, higher-order logic with types, as well as a number of other logics arising in connection to specification languages. The gain for the classical case is that the characterization is proved directly for all signatures, including infinite ones.

    DOI： https://doi.org/10.1093/logcom/exaa042

    Other Link： https://academic.oup.com/logcom/article-abstract/30/7/1377/5900766

  • Stability of termination and sufficient-completeness under pushouts via amalgamation Reviewed International journal

    Theoretical Computer Science   848   82 - 105   2020.9

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    DOI： https://doi.org/10.1016/j.tcs.2020.09.024

    Other Link： https://www.sciencedirect.com/science/article/pii/S0304397520305235?via%3Dihub

  • Birkhoff Completeness for Hybrid-Dynamic First-Order Logic

    28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019 Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, Proceedings   277 - 293   2019.8

    　More details

    Language：English   Publishing type：Research paper (other academic)  

    DOI： 10.1007/978-3-030-29026-9_16

  • Specification and Verification of Invariant Properties of Transition Systems

    Daniel Gaina, Ionut Tutu, Adrian Riesco

    25th Asia-Pacific Software Engineering Conference, APSEC 2018 Proceedings - 25th Asia-Pacific Software Engineering Conference, APSEC 2018   99 - 108   2018.7

    　More details

    Language：English   Publishing type：Research paper (other academic)  

    DOI： 10.1109/APSEC.2018.00024

  • Downward Löwenheim-Skolem Theorem and interpolation in logics with constructors Invited Reviewed International journal

    Daniel Găină

    27 ( 6 )   1717 - 1752   2017.9

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    The present article describes a method for proving Downward Löwenheim-Skolem Theorem within an arbitrary institution satisfying certain logic properties. In order to demonstrate the applicability of the present approach, the abstract results are instantiated to many-sorted first-order logic and preorder algebra. In addition to the first technique for proving Downward Löwenheim-Skolem Theorem, another one is developed, in the spirit of institution-independent model theory, which consists of borrowing the result from a simpler institution across an institution comorphism. As a result, the Downward Löwenheim- Skolem Property is exported from first-order logic to partial algebras, and from higher-order logic with intensional Henkin semantics to higher-order logic with extensional Henkin semantics. The second method successfully extends the domain of application of Downward Löwenheim-Skolem Theorem to other non-conventional logical systems for which the first technique may fail. One major application of Downward Löwenheim-Skolem Theorem is interpolation in constructor-based logics with universally quantified sentences. The interpolation property is established by borrowing it from a base institution for its constructor-based variant across an institution morphism. This result is important as interpolation for constructor-based first-order logics is still an open problem.

    DOI： 10.1093/logcom/exv018

  • Birkhoff style calculi for hybrid logics Reviewed International journal

    Formal Aspects of Computing   29 ( 5 )   805 - 832   2017.9

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1007/s00165-016-0414-y

  • Foundations of logic programming in hybrid logics with user-defined sharing Reviewed International journal

    Theoretical Computer Science   686   1 - 24   2017.7

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1016/j.tcs.2017.04.009

  • Initial semantics in logics with constructors Reviewed International journal

    Journal of Logic and Computation   25 ( 1 )   95 - 116   2015.9

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1093/logcom/exs044

  • Proving sufficient completeness of constructor-based algebraic specifications Reviewed

    Masaki Nakamura, Daniel Gaina, Kazuhiro Ogata, Kokichi Futatsugi

    Lecture Notes in Electrical Engineering   373   15 - 21   2015.1

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1007/978-981-10-0281-6_3

  • Foundations of logic programming in hybridised logics

    22nd International Workshop on Recent Trends in Algebraic Development Techniques, WADT 2014 Recent Trends in Algebraic Development Techniques - 22nd International Workshop, WADT 2014, Revised Selected Papers   69 - 89   2015.1

    　More details

    Language：English   Publishing type：Research paper (other academic)  

    DOI： 10.1007/978-3-319-28114-8_5

  • Forcing, Downward Löwenheim-Skolem and Omitting Types Theorems, Institutionally Reviewed

    8 ( 3-4 )   469 - 498   2014.12

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    In the context of proliferation of many logical systems in the area of mathematical logic and computer science, we present a generalization of forcing in institution-independent model theory which is used to prove two abstract results: Downward Löwenheim-Skolem Theorem (DLST) and Omitting Types Theorem (OTT). We instantiate these general results to many first-order logics, which are, roughly speaking, logics whose sentences can be constructed from atomic formulas by means of Boolean connectives and classical first-order quantifiers. These include first-order logic (FOL), logic of order-sorted algebras (OSA), preorder algebras (POA), as well as their infinitary variants FOL ω1, ω, OSA ω1, ω, POA ω1, ω. In addition to the first technique for proving OTT, we develop another one, in the spirit of institution-independent model theory, which consists of borrowing the Omitting Types Property (OTP) from a simpler institution across an institution comorphism. As a result we export the OTP from FOL to partial algebras (PA) and higher-order logic with Henkin semantics (HNK), and from the institution of FOLω1, ω to PAω1, ω and HNKω1, ω. The second technique successfully extends the domain of application of OTT to non conventional logical systems for which the standard methods may fail.

    DOI： 10.1007/s11787-013-0090-0

  • On automation of OTS/CafeOBJ method Reviewed

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)   8373   578 - 602   2014.1

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1007/978-3-642-54624-2_29

  • Constructor-based inductive theorem prover

    5th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2013 Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Proceedings   328 - 333   2013.10

    　More details

    Language：English   Publishing type：Research paper (other academic)  

    DOI： 10.1007/978-3-642-40206-7-26

  • Interpolation in logics with constructors Reviewed

    Theoretical Computer Science   474   46 - 59   2013.2

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1016/j.tcs.2012.12.002

  • Constructor-based logics Reviewed

    Journal of Universal Computer Science   18 ( 16 )   2204 - 2233   2012.12

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

  • Principles of proof scores in CafeOBJ Invited Reviewed International journal

    Theoretical Computer Science   464   90 - 112   2012.12

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1016/j.tcs.2012.07.041

  • Completeness by forcing Reviewed International journal

    Journal of Logic and Computation   20 ( 6 )   1165 - 1186   2010.12

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1093/logcom/exq012

  • Constructor-based institutions

    3rd International Conference on Algebra and Coalgebra in Computer Science, CALCO 2009 Algebra and Coalgebra in Computer Science - Third International Conference, CALCO 2009, Proceedings   398 - 412   2009.11

    　More details

    Language：English   Publishing type：Research paper (other academic)  

    DOI： 10.1007/978-3-642-03741-2_27

  • Birkhoff completeness in institutions Reviewed International journal

    Logica Universalis   2 ( 2 )   277 - 309   2008.9

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1007/s11787-008-0035-1

  • Erratum An institution-independent generalization of tarski's elementary chain theorem (Journal of Logic and Computation (2006) 16 (713-735) DOI: 10.1093/logcom/exl006) Reviewed

    Journal of Logic and Computation   17 ( 3 )   2007.6

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1093/logcom/exm022

  • An institution-independent proof of the Robinson Consistency Theorem Reviewed International journal

    Studia Logica   85 ( 1 )   41 - 73   2007.2

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1007/s11225-007-9022-4

  • An institution-independent generalization of Tarski's elementary chain theorem Reviewed

    Journal of Logic and Computation   16 ( 6 )   2006.12

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1093/logcom/exl006

▼display all

Presentations

  • Forcing and its applications in hybrid logics Invited International conference

    Section of Mathematical Sciences of the Romanian Academy, the Romanian Mathematical Society, the Simion Stoilow Institute of Mathematics of the Romanian Academy, the Faculty of Mathematics and Computer Science of the University of Bucharest  2019.7 

    　More details

    Event date： 2020.6 - 2020.7

    Language：English  

    Country：Romania  

    Other Link： https://sites.google.com/view/congmatro9/home

  • Birkhoff style proof systems for hybrid-dynamic quantum logic Invited International conference

    Formal verification of quantum circuits/protocols/programs, Japan Advanced Institute for Science and Technology  2024.1 

    　More details

    Event date： 2024.1

    Language：English   Presentation type：Symposium, workshop panel (public)  

    Country：Japan  

  • Initiality in Hybrid-Dynamic Quantum Logic Invited International conference

    Cracow Logic Conference (CLoCk)  2023.6 

    　More details

    Event date： 2023.6

    Language：English   Presentation type：Oral presentation (general)  

    Country：Poland  

  • Robinson consistency in many-sorted hybrid first-order logics International conference

    Advances in Modal Logic, AiML 2022  2022.8 

    　More details

    Event date： 2022.8

    Language：English   Presentation type：Oral presentation (general)  

    Country：France  

  • Stability of termination under pushouts via amalgamation International conference

    Australian and New Zealand Industrial and Applied Mathematics  2022.2 

    　More details

    Event date： 2022.2

    Language：English   Presentation type：Oral presentation (general)  

    Country：Australia  

    Other Link： https://anziam2022.com.au

  • Omitting Types Theorem in hybrid-dynamic first-order logic with rigid symbols International conference

    Mathematical Society of Japan  2021.9 

    　More details

    Event date： 2021.9

    Language：English   Presentation type：Oral presentation (general)  

    Country：Japan  

    Other Link： https://www.mathsoc.jp/en/meeting/chiba21sept/

  • Stability of termination under pushouts via amalgamation

    32nd Seminar on Algebra, Logic and Geometry in Informatics (ALGI)  2021.9 

    　More details

    Event date： 2021.9

    Language：English   Presentation type：Oral presentation (general)  

    Country：Japan  

  • Omitting Types Theorem in hybrid-dynamic first-order logic with rigid symbols International conference

    The Australasian Association for Logic  2021.6 

    　More details

    Event date： 2021.6

    Language：English   Presentation type：Oral presentation (general)  

    Country：Australia  

    Other Link： https://blogs.unimelb.edu.au/logic/aal-2021/

  • Forcing and Calculi for Hybrid Logics International conference

    Australasian Logic Group  2020.12 

    　More details

    Event date： 2020.12

    Language：English  

    Country：Japan  

  • Specification and Verification of Invariant Properties of Transition Systems International conference

    25th Asia-Pacific Software Engineering Conference (APSEC 2018)  2018.12 

    　More details

    Event date： 2020.11

    Language：English  

    Country：Japan  

  • Forcing and Calculi for Hybrid Logics

    31st Seminar on Algebra, Logic and Geometry in Informatics (ALGI)  2020.9 

    　More details

    Event date： 2020.9

    Language：English  

    Country：Japan  

    Other Link： https://sites.google.com/site/algimeeting/home/31/program

  • Specification and Verification of Invariant Properties of Transition Systems Invited International conference

    Working Formal Methods Symposium (FROM 2017)  2017.7 

    　More details

    Event date： 2020.7

    Language：English   Presentation type：Oral presentation (general)  

    Country：Romania  

    Other Link： http://unibuc.ro/~conference/from2017/#2

  • Horn Clauses in Hybrid-Dynamic First-Order Logic

    The 15th Theorem Proving and Provers meeting (TPP 2019)  2019.11 

    　More details

    Event date： 2019.11

    Language：English  

    Country：Japan  

    Other Link： https://akihisayamada.github.io/tpp2019/

  • Birkhoff Completeness for Hybrid-Dynamic First-Order Logic

    The 18th Logic and Computation Seminar  2019.11 

    　More details

    Event date： 2019.11

    Language：English  

    Country：Japan  

    Other Link： https://lcseminar.wordpress.com/2019/11/12/lcseminar18/

  • Mathematical structures for developing reconfigurable systems International conference

    La Trobe - Kyushy Joint Seminar on Mathematics for Industry  2017.5 

    　More details

    Event date： 2017.5

    Language：English  

    Country：Japan  

▼display all

Works

Professional Memberships

  • Mathematical Society of Japan

Academic Activities

  • Program Committee member International contribution

    International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols FAVPQC 2022  （ Madrid Spain ） 2022.10

    　More details

    Type：Competition, symposium, etc. 

  • Screening of academic papers

    Role(s)： Peer review

    2022

    　More details

    Type：Peer review 

    Proceedings of International Conference Number of peer-reviewed papers：1

    Proceedings of domestic conference Number of peer-reviewed papers：3

  • Screening of academic papers

    Role(s)： Peer review

    2021

    　More details

    Type：Peer review 

    Proceedings of International Conference Number of peer-reviewed papers：1

    Proceedings of domestic conference Number of peer-reviewed papers：3

  • Programme Committee member International contribution

    8th Conference on Algebra and Coalgebra in Computer Science CALCO 2019  （ London UnitedKingdom ） 2019.6

    　More details

    Type：Competition, symposium, etc. 

  • Screening of academic papers

    Role(s)： Peer review

    2019

    　More details

    Type：Peer review 

    Number of peer-reviewed articles in foreign language journals：1

    Proceedings of International Conference Number of peer-reviewed papers：3

    Proceedings of domestic conference Number of peer-reviewed papers：3

Research Projects

  • A theorem prover for the correct development of reconfigurable systems International coauthorship

    2023.4 - 2027.4

    　 More details

    Authorship：Principal investigator 

  • A theorem prover for the correct development of reconfigurable systems

    Grant number：60050  2023 - 2026

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research  Grant-in-Aid for Scientific Research (C)

    　 More details

    Authorship：Principal investigator  Grant type：Scientific research funding

  • Mathematical foundations for the reconfiguration paradigm International coauthorship

    2020.4 - 2024.3

    　 More details

    Authorship：Principal investigator 

  • Mathematical foundations for the reconfiguration paradigm

    Grant number：12030  2020 - 2024

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research  Grant-in-Aid for Scientific Research (C)

    　 More details

    Authorship：Principal investigator  Grant type：Scientific research funding

  • The relationship between gaining expressive power in extending first-order logics and losing 'control' over the extension International coauthorship

    2018.4 - 2021.3

    　 More details

    Authorship：Principal investigator 

    The purpose of this project is to complete the work started by Lindstrom on the expressivity of first-order logic by making his result not only syntactic-free but also semantic-free in the spirit of abstract model theory.

Educational Activities

  • I have taught a variety of applied mathematical subjects such as algebraic specification, model theoretic topics for the design of specification and verification languages, or term rewriting. I organize lectures in collaboration with other universities such as La Trobe University. I also supervise graduate research students.

Class subject

  • 情報数学特論１

    2024.10 - 2025.3   Second semester

  • 数理科学特論１９

    2024.4 - 2024.9   First semester

  • MMA数学特論II

    2024.4 - 2024.9   First semester

  • 数学共創概論Ⅱ

    2023.10 - 2024.3   Second semester

  • 機能数理学概論Ⅰ

    2023.10 - 2024.3   Second semester

  • MMA数学特論II

    2023.10 - 2024.3   Second semester

  • 数理科学特論１９

    2023.10 - 2024.3   Second semester

  • 数学共創概論Ⅱ

    2023.10 - 2024.3   Second semester

  • 機能数理学概論Ⅰ

    2023.10 - 2024.3   Second semester

  • MMA数学特論II

    2023.10 - 2024.3   Second semester

  • 数理科学特論１９

    2023.10 - 2024.3   Second semester

  • 数学創発モデリング

    2023.4 - 2024.3   Full year

  • 数学創発モデリング

    2023.4 - 2024.3   Full year

  • 計算数理学Ⅰ

    2023.4 - 2023.9   First semester

  • ルベーグ積分

    2023.4 - 2023.9   First semester

  • 計算数理学Ⅰ

    2023.4 - 2023.9   First semester

  • ルベーグ積分

    2023.4 - 2023.9   First semester

  • Functional Mathematics I

    2022.10 - 2023.3   Second semester

  • Functional Mathematics I

    2022.10 - 2023.3   Second semester

  • 数学共創概論Ⅱ

    2022.10 - 2023.3   Second semester

  • 機能数理学概論Ⅰ

    2022.10 - 2023.3   Second semester

  • MMA数学特論II

    2022.10 - 2023.3   Second semester

  • 数理科学特論１９

    2022.10 - 2023.3   Second semester

  • 数学共創モデリング

    2022.4 - 2023.3   Full year

  • 数学共創モデリング

    2022.4 - 2023.3   Full year

  • Topics in Computational Mathematics I

    2022.4 - 2022.9   First semester

  • Topics in Computational Mathematics I

    2022.4 - 2022.9   First semester

  • Topics in Computational Mathematics I

    2022.4 - 2022.9   First semester

  • 計算数理学Ⅰ

    2022.4 - 2022.9   First semester

  • 計算数理学Ⅰ

    2022.4 - 2022.9   First semester

  • 応用数学A

    2022.4 - 2022.9   First semester

  • 機能数理学概論Ⅰ

    2021.10 - 2022.3   Second semester

  • MMA数学特論II

    2021.10 - 2022.3   Second semester

  • 数理科学特論１９

    2021.10 - 2022.3   Second semester

  • 機能数理学概論Ⅰ

    2021.10 - 2022.3   Second semester

  • MMA数学特論II

    2021.10 - 2022.3   Second semester

  • 数理科学特論１９

    2021.10 - 2022.3   Second semester

  • 機能数理学概論Ⅰ

    2021.10 - 2022.3   Second semester

  • MMA数学特論II

    2021.10 - 2022.3   Second semester

  • 数理科学特論１９

    2021.10 - 2022.3   Second semester

  • 計算数理学Ⅰ

    2021.4 - 2021.9   First semester

  • 応用数学A

    2021.4 - 2021.9   First semester

  • 計算数理学Ⅰ

    2021.4 - 2021.9   First semester

  • 応用数学A

    2021.4 - 2021.9   First semester

  • 計算数理学Ⅰ

    2021.4 - 2021.9   First semester

  • 応用数学A

    2021.4 - 2021.9   First semester

  • [M2]Topics in Computational Mathematics I

    2021.4 - 2021.9   First semester

  • [M2]計算数理学Ⅰ

    2021.4 - 2021.9   First semester

  • MMA数学特論Ⅱ

    2020.10 - 2021.3   Second semester

  • 数理科学特論１９

    2020.10 - 2021.3   Second semester

  • 機能数理学概論Ⅰ

    2020.4 - 2020.9   First semester

  • 応用数学Ⅱ

    2020.4 - 2020.9   First semester

  • MMA数学入門

    2020.4 - 2020.9   First semester

  • MMA数学入門

    2020.4 - 2020.9   First semester

  • MMA数学入門

    2020.4 - 2020.9   First semester

▼display all

Other educational activity and Special note

  • 2023  Coaching of Students' Association 

Outline of Social Contribution and International Cooperation activities

  • I am involved in research collaborations with European and Australian academics as well as with Japanese researchers.
    I organize an online seminar for the development of a software tool for the specification and verification of reconfigurable systems. My collaborators for this project are Adrian Riesco (Complutense University of Madrid) and Ionut Tutu (Institute of Mathematics of the Romanian Academy).
    I work with Tomasz Kowalski (Jagiellonian University, Poland) and Guillermo Badia (The University of Queensland) on a project where we study the relationship between gaining expressive power in extending first-order logics and losing 'control' over the extension.
    I am involved in the organization of joint research seminars with Mathematics and Statistics Department of La Trobe University.

Activities contributing to policy formation, academic promotion, etc.

  • 2018.2   Co-organized by the Institute of Mathematics for Industry at Kyushu University and La Trobe University

    Main organizer of the international “Workshop on Logic, Algebra and Category Theory”, Melbourne, February 12-16, 2018

Travel Abroad

  • 2022.8 - 2022.9

    Staying countory name 1：Romania   Staying institution name 1：Institute of Mathematics of the Romanian Academy

  • 2022.8

    Staying countory name 1：France   Staying institution name 1：The french laboratory for research and innovation in digital science and technology (IRISA)