Tatsuta Makoto 龍田真

… Alternative Names

龍田真タツタマコト

TATSUTA Makoto 龍田真

Less

Researcher Number	80216994
External Links
Affiliation (Current)	2025: 国立情報学研究所, 情報学プリンシプル研究系, 教授
Affiliation (based on the past Project Information) *help	2025: 国立情報学研究所, 情報学プリンシプル研究系, 教授 2018 – 2023: 国立情報学研究所, 情報学プリンシプル研究系, 教授 2007 – 2016: National Institute of Informatics, 情報学プリンシプル研究系, 教授 2001 – 2003: 国立情報学研究所, 情報学基礎研究系, 教授 1996 – 2000: 京都大学, 大学院・理学研究科, 助教授 … More 1998: 京都大学, 大学院理学研究科, 助教授 1996 – 1997: 京都大学, 理学研究科, 助教授 1994 – 1995: 東北大学, 電気通信研究所, 助教授 1990 – 1993: 東北大学, 電気通信研究所, 助手 Less
Review Section/Research Field	Principal Investigator 計算機科学 / Basic Section 60050:Software-related / Basic Section 60010:Theory of informatics-related / Theory of informatics / Fundamental theory of informatics / General mathematics (including Probability theory/Statistical mathematics) Except Principal Investigator 計算機科学 / General mathematics (including Probability theory/Statistical mathematics) / Science and Engineering
Keywords	Principal Investigator プログラム理論 / 実現可能性解釈 / プログラム合成 / 帰納的定義 / ソフトウェア検証 / 分離論理 / 型理論 / メモリ安全性 / ソフトウェア解析 / 置換簡約 … More / 余帰納的定義 / プログラム論理 / 数理論理 / 記号ヒープ / Permutative reductions / Strong normalization / Theory of programs / Type theory / Constructive logic / 構成的集合 / 強正規化可能性 / 構成的論理 / イタリア / シンガポール / 国際情報交換 / 存在型 / 構成的プログラミング / 直観主義論理 … More Except Principal Investigator Constructive Programming / 構成的プログラミング / 直観主義論理 / 型理論 / Catch / 関数型プログラム言語 / 構成的論理 / 宣言的プログラミング / ソフトウェア発展 / lambda calculus / bounded arithmetic / reverse mathematics / second order arithmetic / formal arithmetic / type theory / theory of computation / logical structures / 数学基礎論 / 算術のモデル / 証明論 / ロジック / ラムダ計算 / 限定算術 / 逆数学 / 2階算術 / 形式算術 / 計算論 / 論理構造 / Modal Logic / Classical Logic / Intuitionistic Logic / Interactive Proof System / 証明エンジン / グラフィカルユーザインターフェース / 証明支援システム / 様相論理 / 古典論理 / 対話的証明環境 / Type Theory / Throwcontrd / Throw機構 / キャッチスロー機構 / Lazy evaluation / Assignment Statement / Functional Programming / Proof Development System / Constructive Logic / プログラム合成 / プログラム検証 / 関数型プロゲーム言語 / 遅延評価 / 代入文 / 証明システム / Graph theory / Type theory / Constructive logic / Theory of programs / グラフ理論 / プログラム理論 / 関数型プログラミング / デフォルト論理 / 仮説論理プログラム / 極小更新 Less

循環証明の証明変換Principal Investigator
- Principal Investigator
  
  龍田真
- Project Period (FY)
  2025 – 2029
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Review Section
  
  Basic Section 60010:Theory of informatics-related
- Research Institution
  National Institute of Informatics
分離論理を用いたソフトウェア検証の発展Principal Investigator
- Principal Investigator
  
  龍田真
- Project Period (FY)
  2021 – 2023
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Review Section
  
  Basic Section 60050:Software-related
- Research Institution
  National Institute of Informatics
Software verification system by separation logicPrincipal Investigator
- Principal Investigator
  
  Tatsuta Makoto
- Project Period (FY)
  2018 – 2020
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Review Section
  
  Basic Section 60050:Software-related
- Research Institution
  National Institute of Informatics
Theory of software verification by separation logicPrincipal Investigator
- Principal Investigator
  
  Tatsuta Makoto
- Project Period (FY)
  2015 – 2016
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  Theory of informatics
- Research Institution
  National Institute of Informatics
Type Theory of Existential TypesPrincipal Investigator
- Principal Investigator
  
  TATSUTA Makoto
- Project Period (FY)
  2011 – 2014
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  Fundamental theory of informatics
- Research Institution
  National Institute of Informatics
Type Theory of Commutative ReductionsPrincipal Investigator
- Principal Investigator
  
  TATSUTA Makoto
- Project Period (FY)
  2007 – 2010
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  General mathematics (including Probability theory/Statistical mathematics)
- Research Institution
  National Institute of Informatics
宣言的プログラミングにおけるソフトウェア発展の研究
- Principal Investigator
  
  佐藤健
- Project Period (FY)
  2002
- Research Category
  
  Grant-in-Aid for Scientific Research on Priority Areas
- Review Section
  
  Science and Engineering
- Research Institution
  National Institute of Informatics
宣言的プログラミングにおけるソフトウェア発展の研究
- Principal Investigator
  
  佐藤健
- Project Period (FY)
  2001
- Research Category
  
  Grant-in-Aid for Scientific Research on Priority Areas (C)
- Review Section
  
  Science and Engineering
- Research Institution
  National Institute of Informatics
Program synthesis using constructive sets and coinductive definitionsPrincipal Investigator
- Principal Investigator
  
  TATSUTA Makoto
- Project Period (FY)
  2000 – 2003
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  計算機科学
- Research Institution
  National Institute of Informatics
  Kyoto University
帰納的定義を用いたプログラム合成Principal Investigator
- Principal Investigator
  
  龍田真
- Project Period (FY)
  1997 – 1998
- Research Category
  
  Grant-in-Aid for Encouragement of Young Scientists (A)
- Research Field
  
  計算機科学
- Research Institution
  Kyoto University
Studies on logical structures of arithmetic and computation
- Principal Investigator
  
  TANAKA Kazuyuki
- Project Period (FY)
  1997 – 1999
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Research Field
  
  General mathematics (including Probability theory/Statistical mathematics)
- Research Institution
  TOHOKU UNIVERSITY
帰納的定義を用いたプログラム合成Principal Investigator
- Principal Investigator
  
  龍田真
- Project Period (FY)
  1996
- Research Category
  
  Grant-in-Aid for Encouragement of Young Scientists (A)
- Research Field
  
  計算機科学
- Research Institution
  Kyoto University
Theory of Constructive Programming
- Principal Investigator
  
  SATO Masahiko
- Project Period (FY)
  1996 – 1997
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Research Field
  
  計算機科学
- Research Institution
  KYOTO UNIVERSITY
Design and Implementation of Constructive Programming Systems
- Principal Investigator
  
  SATO Masahiko
- Project Period (FY)
  1996 – 1997
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Research Field
  
  計算機科学
- Research Institution
  KYOTO UNIVERSITY
帰納的定義を用いたプログラム合成Principal Investigator
- Principal Investigator
  
  龍田真
- Project Period (FY)
  1995
- Research Category
  
  Grant-in-Aid for Encouragement of Young Scientists (A)
- Research Field
  
  計算機科学
- Research Institution
  Tohoku University
帰納的定義を用いたプログラム合成Principal Investigator
- Principal Investigator
  
  龍田真
- Project Period (FY)
  1994
- Research Category
  
  Grant-in-Aid for Encouragement of Young Scientists (A)
- Research Field
  
  計算機科学
- Research Institution
  Tohoku University
Constructive Programming System for Proof Development, Verification, and Program Synthesis
- Principal Investigator
  
  SATO Masahiko
- Project Period (FY)
  1994 – 1995
- Research Category
  
  Grant-in-Aid for General Scientific Research (B)
- Research Field
  
  計算機科学
- Research Institution
  KYOTO UNIVERSITY
  Tohoku University
帰納的定義を用いたプログラム合成Principal Investigator
- Principal Investigator
  
  龍田真
- Project Period (FY)
  1993
- Research Category
  
  Grant-in-Aid for Encouragement of Young Scientists (A)
- Research Field
  
  計算機科学
- Research Institution
  Tohoku University
Co-operative research on foundational theories of programs
- Principal Investigator
  
  SATO Masahiko
- Project Period (FY)
  1990 – 1992
- Research Category
  
  Grant-in-Aid for Co-operative Research (A)
- Research Field
  
  General mathematics (including Probability theory/Statistical mathematics)
- Research Institution
  Tohoku University

All 2023 2022 2021 2019 2018 2016 2015 2014 2013 2011 2010 2009 2008 2007

All Journal Article Presentation

[Journal Article] 帰納法に関する推論の計算複雑性2023
- Author(s)
  伊藤宗平,　龍田真
- Journal Title
  
  Proceedings of the 24th JSSST Workshop on Programming and Programming Languages (PPL2023)
  
  Volume: 1
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-21H03421
[Journal Article] Biabduction for Separation Logic with Arrays and Lists2022
- Author(s)
  Daisuke Kimura, Makoto Tatsuta, Mahmudul Faisal Al Ameen, Koji Nakazawa, and Mirai Ikebuchi
- Journal Title
  
  Proceedings of the 24st JSSST Workshop on Programming and Programming Languages (PPL2021)
  
  Volume: 1
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-18H03226
[Journal Article] Biabduction for Separation Logic with Arrays and Lists2022
- Author(s)
  Daisuke Kimura, Makoto Tatsuta, Mahmudul Faisal Al Ameen, oji Nakazawa, and Mirai Ikebuchi
- Journal Title
  
  Biabduction for Separation Logic with Arrays and Lists
  
  Volume: 1
- Peer Reviewed / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-21H03421
[Journal Article] Biabduction for Separation Logic with Arrays and Lists2022
- Author(s)
  Daisuke Kimura, Makoto Tatsuta, Mahmudul Faisal Al Ameen, Koji Nakazawa, and Mirai Ikebuchi
- Journal Title
  
  Proceedings of the 24th JSSST Workshop on Programming ad Programming Languages (PPL2022)
  
  Volume: -
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-18H03226
[Journal Article] 帰納的推論の計算複雑性2022
- Author(s)
  伊藤宗平,　龍田真
- Journal Title
  
  ソフトウェア科学会第39回大会論文集
  
  Volume: 1
- Data Source
  KAKENHI-PROJECT-21H03421
[Journal Article] Decidability for Entailments of Symbolic Heaps with Arrays2021
- Author(s)
  Daisuke Kimura, Makoto Tatsuta
- Journal Title
  
  Logical Methods in Computer Science
  
  Volume: 17 (2)
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-18H03226
[Journal Article] Function Pointer Eliminator for C Programs2021
- Author(s)
  Daisuke Kimura, Mahmudul Faisal Al Ameen, Makoto Tatsuta, and Koji Nakazawa
- Journal Title
  
  Lecture Notes in Computer Science
  
  Volume: 13008 Pages: 23-37
- DOI
  10.1007/978-3-030-89051-3_2
- ISBN
  9783030890506, 9783030890513
- Peer Reviewed / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-18H03226, KAKENHI-PROJECT-21H03421
[Journal Article] Decidability for Entailments of Symbolic Heaps with Arrays2021
- Author(s)
  Daisuke Kimura, Makoto Tatsuta
- Journal Title
  
  Logical Methods in Computer Science
  
  Volume: 17 (2)
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-21H03421
[Journal Article] Spatial Factorization in Cyclic-Proof System for Separation Logic2019
- Author(s)
  Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, and Mitsuru Yamamura
- Journal Title
  
  Proceedings of the 21st JSSST Workshop on Programming and Programming Languages (PPL2019)
  
  Volume: 1
- NAID
  130007801472
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-18H03226
[Journal Article] Intuitionistic Podelski-Rybalchenko Theorem and Equivalence between Inductive Definitions and Cyclic Proofs2018
- Author(s)
  Stefano Berardi and Makoto Tatsuta
- Journal Title
  
  LNCS
  
  Volume: 11202 Pages: 13-33
- DOI
  10.1007/978-3-030-00389-0_3
- ISBN
  9783030003883, 9783030003890
- Peer Reviewed / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-18H03226
[Journal Article] Completeness for Recursive Procedures in Separation Logic2016
- Author(s)
  Mahmudul Faisal Al Ameen and Makoto Tatsuta
- Journal Title
  
  Theoretical Computer Science
  
  Volume: 631 Pages: 73-96
- DOI
  10.1016/j.tcs.2016.04.004
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-15K00027
[Journal Article] Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic2016
- Author(s)
  Makoto Tatsuta, Quang Loc Le, and Wei-Ngan Chin
- Journal Title
  
  Lecture Notes in Computer Science
  
  Volume: 10017 Pages: 423-443
- DOI
  10.1007/978-3-319-47958-3_22
- ISBN
  9783319479576, 9783319479583
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-15K00027
[Journal Article] Translation of Symbolic Heaps with Monadic Inductive Definitions into Monadic Second-Order Logic2016
- Author(s)
  Makoto Tatsuta and Daisuke Kimura
- Journal Title
  
  Proceedings of the 18th JSSST Workshop on Programming and Programming Languages
  
  Volume: 1
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-15K00027
[Journal Article] Separation Logic with Monadic Inductive Definitions and Implicit Existentials2015
- Author(s)
  Makoto Tatsuta and Daisuke Kimura
- Journal Title
  
  Lecture Notes in Computer Science
  
  Volume: 9458
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-15K00027
[Journal Article] Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics2013
- Author(s)
  Stefano Berardi and Makoto Tatsuta
- Journal Title
  
  Lecture Notes in Computer Science
  
  Volume: 7941 Pages: 61-76
- DOI
  10.1007/978-3-642-38946-7_7
- ISBN
  9783642389450, 9783642389467
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-23500030
[Journal Article] Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types2013
- Author(s)
  Daisuke Kimura and Makoto Tatsuta
- Journal Title
  
  Logical Methods in Computer Science
  
  Volume: 9
- DOI
  10.2168/lmcs-9(1:14)2013
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-23500030
[Journal Article] Static Analysis for Multi-Staged Programs via Unstaging Translation2011
- Author(s)
  Wontae Choi, Baris Aktemur, Kwangkeun Yi, Makoto Tatsuta
- Journal Title
  
  Proceedings of 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 2011) 81--92.
  
  Volume: 全1巻 Pages: 81-92
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19540156
[Journal Article] Type Inference for Bimorphic Recursion2011
- Author(s)
  Makoto Tatsuta and Ferruccio Damiani
- Journal Title
  
  Electronic Proceedings in Theoretical Computer Science
  
  Volume: 54
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-23500030
[Journal Article] Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems2010
- Author(s)
  Koji Nakazawa, Makoto Tatsuta
- Journal Title
  
  Chicago Journal of Theoretical Computer Science
  
  Volume: (Article 7)
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19540156
[Journal Article] Internal Normalization, Compilation and Decompilation for System F2010
- Author(s)
  Stefano Berardi, Makoto Tatsuta
- Journal Title
  
  Lecture Notes in Computer Science
  
  Volume: 6009 Pages: 207-223
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19540156
[Journal Article] Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems2010
- Author(s)
  Koji Nakazawa, Makoto Tatsuta
- Journal Title
  
  Chicago Journal of Theoretical Computer Science Article 7
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19540156
[Journal Article] Inhabitation of Polymorphic and Existential Types2010
- Author(s)
  Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa, Hiroshi Nakano
- Journal Title
  
  \em Annals of Pure and Applied Logic (to appear)
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19540156
[Journal Article] Inhabitation of Polymorphic and Existential Types2010
- Author(s)
  Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa, Hiroshi Nakano
- Journal Title
  
  Annals of Pure and Applied Logic (出版確定)
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19540156
[Journal Article] Inhabitation of Polymorphic and Existential Types2010
- Author(s)
  Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa, Hiroshi Nakano
- Journal Title
  
  Annals of Pure and Applied Logic 161(11)
  
  Pages: 1390-1399
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19540156
[Journal Article] Internal Normalization, Compilation and Decompilation for System F2010
- Author(s)
  Stefano Berardi, Makoto Tatsuta
- Journal Title
  
  Lecture Notes in Computer Science(In : Proceedings of Tenth International Symposium on Functional and Logic Programming (FLOPS 2010)) 6009
  
  Pages: 207-223
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19540156
[Journal Article] On Isomorphisms of Intersection Types2010
- Author(s)
  Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, Makoto Tatsuta
- Journal Title
  
  ACM Transactions on Computational Logic 11(4) Article No 25
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19540156
[Journal Article] On Isomorphisms of Intersection Types2010
- Author(s)
  M.Dezani-Ciancaglini, R.Di Cosmo, E.Giovannetti, M.Tatsuta
- Journal Title
  
  ACM Transactions on Computational Logic (出版確定)
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19540156
[Journal Article] Non-Commutative First-Order Sequent Calculus2009
- Author(s)
  Makoto Tatsuta
- Journal Title
  
  Lecture Notes in Computer Science(In : Proceedings of 18th EACSL Annual Conference on Computer Science Logic (CSL2009)) 5771
  
  Pages: 470-484
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19540156
[Journal Article] Non-Commutative First-Order Sequent Calculus2009
- Author(s)
  Makoto Tatsuta
- Journal Title
  
  Lecture Notes in Computer Science 5771
  
  Pages: 470-484
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19540156
[Journal Article] Proceedings of 18th EACSL Annual Conference on Computer Science Logic (CSL2009)2009
- Author(s)
  Makoto Tatsuta, Non-Commutative First-Order Sequent Calculus
- Journal Title
  
  Lecture Notes in Computer Science 5771
  
  Pages: 470-484
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19540156
[Journal Article] Types for Hereditary Permutators2008
- Author(s)
  Makoto Tatsuta
- Journal Title
  
  Proceedings of Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS 2008)
  
  Pages: 83-92
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19540156
[Journal Article] Strong normalization of classical natural deduction with disjunctions2008
- Author(s)
  Koji Nakazawa, Makoto Tatsuta
- Journal Title
  
  Annals of Pure and Applied Logic 153(1-3)
  
  Pages: 21-37
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19540156
[Journal Article] On Isomorphisms of Intersection Types2008
- Author(s)
  M. Dezani-Ciancaglini, R. Di Cosmo, E. Giovannetti., M. Tatsuta
- Journal Title
  
  Leeture Notes in Computer Science 5213
  
  Pages: 461-477
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19540156
[Journal Article] Types for Hereditary Permutators2008
- Author(s)
  Makoto Tatsuta
- Journal Title
  
  In : Proceedings of Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS2008)
  
  Pages: 83-92
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19540156
[Journal Article] Simple saturated sets for disjunction and second-order existential quantification2007
- Author(s)
  M.Tatsuta
- Journal Title
  
  Lecture Notes in Computer Science(In : Proceedings of 8th International Conference on Typed Lambda Calculi and Applications (TLCA 2007)) 4583
  
  Pages: 366-380
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19540156
[Journal Article] The maximum length of mu-reduction in lambda mu-alculus2007
- Author(s)
  Makoto Tatsuta
- Journal Title
  
  Lecture Notes in Computer Science 4533
  
  Pages: 359-373
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19540156
[Journal Article] Simple saturated sets for disjunction and second-order existential quantification2007
- Author(s)
  M. Tatsuta
- Journal Title
  
  Lecture Notes in Computer Science 4583
  
  Pages: 366-380
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19540156
[Presentation] Brotherston's Conjecture: Equivalence of Inductive Definitions and Cyclic Proofs2022
- Author(s)
  Makoto Tatsuta
- Organizer
  九州大学論理と計算セミナー
- Data Source
  KAKENHI-PROJECT-18H03226
[Presentation] Brotherston's Conjecture: Equivalence of Inductive Definitions and Cyclic Proofs2022
- Author(s)
  Makoto Tatsuta
- Organizer
  九州大学論理と計算セミナー
- Data Source
  KAKENHI-PROJECT-21H03421
[Presentation] 帰納的定義付き一階述語論理の循環証明体系におけるカット除去2021
- Author(s)
  益岡幸弘, 龍田真
- Organizer
  記号論理学と情報科学研究集会(SLACS 2021)
- Data Source
  KAKENHI-PROJECT-21H03421
[Presentation] Cut-elimination in cyclic proof system for first-order logic2021
- Author(s)
  Yukihiro Masuoka and Makoto Tatsuta
- Organizer
  Fourth Workshop on Mathematical Logic and its Applications (MLA 2021)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-18H03226
[Presentation] 帰納的定義付き一階述語論理の循環証明体系におけるカット除去2021
- Author(s)
  益岡幸弘, 龍田真
- Organizer
  記号論理学と情報科学研究集会(SLACS 2021)
- Data Source
  KAKENHI-PROJECT-18H03226
[Presentation] Completeness of Cyclic Proofs for Symbolic Heaps with Cone Inductive Definitions2019
- Author(s)
  Makoto Tatsuta
- Organizer
  Third Workshop on Mathematical Logic and its Applications (MLA 2019)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-18H03226
[Presentation] Decidable subsystem of Presburger Arithmetic with Inductive Definitions and Application to Symbolic Heaps2016
- Author(s)
  Makoto Tatsuta
- Organizer
  International Workshop on Mathematics for Computation (M4C)
- Place of Presentation
  Niederalteich, Germany
- Year and Date
  2016-05-08
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-15K00027
[Presentation] Decidability and Undecidability in Symbolic-Heap System with Inductive Definitions2015
- Author(s)
  Makoto Tatsuta and Daisuke Kimura
- Organizer
  Continuity, Computability, Constructivity: From Logic to Algorithms (CCC2015)
- Place of Presentation
  Kochel, Germany
- Year and Date
  2015-09-16
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-15K00027
[Presentation] Realizability of inductive and coinductive definitions2015
- Author(s)
  Makoto Tatsuta
- Organizer
  JAIST Logic Workshop Series 2015: Constructivism and Computability
- Place of Presentation
  しいのき迎賓館(石川県金沢市広坂２－１－１)
- Year and Date
  2015-03-03
- Invited
- Data Source
  KAKENHI-PROJECT-23500030
[Presentation] Completeness of second-order separation logic for program verification2014
- Author(s)
  Makoto Tatsuta, and Wei-Ngan Chin
- Organizer
  Logic Colloquium 2014
- Place of Presentation
  Vienna, Austria
- Year and Date
  2014-07-15
- Data Source
  KAKENHI-PROJECT-23500030
[Presentation] 遺伝的置換子の型とTLCA未解決問題20番2008
- Author(s)
  龍田真
- Organizer
  日本ソフトウェア科学会第25回大会(査読無)
- Data Source
  KAKENHI-PROJECT-19540156

1. SATO Masahiko (20027387)

# of Collaborated Projects: 4 results

# of Collaborated Products: 0 results
2. KAMEYAMA Yukiyoshi (10195000)

# of Collaborated Projects: 4 results

# of Collaborated Products: 0 results
3. NAKAZAWA Koji (80362581)

# of Collaborated Projects: 2 results

# of Collaborated Products: 1 results
4. TAKEUTI Izumi (20264583)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
5. KIMURA Daisuke (90455197)

# of Collaborated Projects: 2 results

# of Collaborated Products: 5 results
6. 佐藤健 (00271635)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
7. 新井紀子 (40264931)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
8. 照井一成 (70353422)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
9. SAWAMURA Hajime (40282991)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
10. TANAKA Kazuyuki (70188291)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
11. KASHIMA Ryo (10240756)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
12. HORAI Masako (00015588)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
13. AKAMA Yohji (30272454)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
14. HASEGAWA Ryu (20243107)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
15. 廣川佐千男 (40126785)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
16. 安本雅洋 (10144114)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
17. 菊池誠 (60273801)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
18. OHTANI Takeshi

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results

Tatsuta Makoto 龍田 真

龍田 真 タツタ マコト

TATSUTA Makoto 龍田 真

Research Projects

Research Products

Co-Researchers

循環証明の証明変換Principal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

分離論理を用いたソフトウェア検証の発展Principal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Software verification system by separation logicPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Theory of software verification by separation logicPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Type Theory of Existential TypesPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Type Theory of Commutative ReductionsPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

宣言的プログラミングにおけるソフトウェア発展の研究

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

宣言的プログラミングにおけるソフトウェア発展の研究

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Program synthesis using constructive sets and coinductive definitionsPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

帰納的定義を用いたプログラム合成Principal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Studies on logical structures of arithmetic and computation

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

帰納的定義を用いたプログラム合成Principal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Theory of Constructive Programming

Principal Investigator

Tatsuta Makoto 龍田真

龍田真タツタマコト

TATSUTA Makoto 龍田真