KIMURA Daisuke 木村大輔

… Alternative Names

木村大輔キムラダイスケ

Less

Researcher Number	90455197
Other IDs	https://orcid.org/0000-0001-6287-692X
Affiliation (Current)	2026: 東邦大学, 理学部, 准教授
Affiliation (based on the past Project Information) *help	2026: 東邦大学, 理学部, 准教授 2022 – 2024: 東邦大学, 理学部, 准教授 2018 – 2022: 東邦大学, 理学部, 講師 2016: 東邦大学, 理学部情報科学科, 講師
Review Section/Research Field	Principal Investigator Basic Section 60010:Theory of informatics-related Except Principal Investigator Basic Section 60010:Theory of informatics-related / Basic Section 60050:Software-related / Theory of informatics
Keywords	Except Principal Investigator 分離論理 / ソフトウェア検証 / 帰納的述語 / カット除去 / メモリ安全性 / ソフトウェア解析 / 証明体系 / 不動点演算子 / カット除去可能性 / 循環証明体系 … More / 証明論 / シーケント計算 / 循環証明 / カット除去定理 / 数理論理 / 帰納的定義 / 記号ヒープ Less

循環証明体系の計算論的分析Principal Investigator
- Principal Investigator
  
  木村大輔
- Project Period (FY)
  2026 – 2029
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Review Section
  
  Basic Section 60010:Theory of informatics-related
- Research Institution
  Toho University
循環証明体系におけるカット除去定理とカット規則の制限
- Principal Investigator
  
  中澤巧爾
- Project Period (FY)
  2022 – 2025
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Review Section
  
  Basic Section 60010:Theory of informatics-related
- Research Institution
  Nagoya University
Development for software verification by separation logic
- Principal Investigator
  
  Tatsuta Makoto
- 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
Proof theoretic analysis of cyclic proof systems
- Principal Investigator
  
  Nakazawa Koji
- Project Period (FY)
  2018 – 2020
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Review Section
  
  Basic Section 60010:Theory of informatics-related
- Research Institution
  Nagoya University
Theory of software verification by separation logic
- 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

All 2024 2022 2021 2020 2019 2016 2015

All Journal Article Presentation

[Journal Article] Restriction on cut rule in cyclic-proof system for symbolic heaps2024
- Author(s)
  Saotome Kenji、Nakazawa Koji、Kimura Daisuke
- Journal Title
  
  Theoretical Computer Science
  
  Volume: 1019 Pages: 1-22
- DOI
  10.1016/j.tcs.2024.114854
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-24K02900, KAKENHI-PROJECT-22K11901
[Journal Article] Cut-elimination for cyclic proof systems with inductively defined propositions2022
- Author(s)
  Daisuke Kimura, Koji Nakazawa, and Kenji Saotome
- Journal Title
  
  RIMS Kokyuroku
  
  Volume: 2228 Pages: 30-40
- Open Access
- Data Source
  KAKENHI-PROJECT-22K11901
[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] Decidability for Entailments of Symbolic Heaps with Arrays2021
- Author(s)
  Daisuke Kimura, Makoto Tatsuta
- Journal Title
  
  Logical Methods in Computer Science
  
  Volume: 17 (2)
- DOI
  10.23638/lmcs-17(2:15)2021
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-18H03226, KAKENHI-PROJECT-21H03421
[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] Restriction on Cut in Cyclic Proof System for Symbolic Heaps2020
- Author(s)
  Saotome Kenji、Nakazawa Koji、Kimura Daisuke
- Journal Title
  
  FLOPS 2020, Lecture Notes in Computer Science
  
  Volume: 12073 Pages: 88-105
- DOI
  10.1007/978-3-030-59025-3_6
- ISBN
  9783030590246, 9783030590253
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-18K11161
[Journal Article] Failure of Cut-Elimination in Cyclic Proofs of Separation Logic2020
- Author(s)
  KIMURA Daisuke、NAKAZAWA Koji、TERAUCHI Tachio、UNNO Hiroshi
- Journal Title
  
  Computer Software
  
  Volume: 37 Issue: 1 Pages: 1_39-1_52
- DOI
  10.11309/jssst.37.1_39
- NAID
  130007815024
- ISSN
  0289-6540
- Year and Date
  2020-01-24
- Language
  Japanese
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-18K11161, KAKENHI-PROJECT-18K19787, KAKENHI-PROJECT-17H01720, KAKENHI-PROJECT-17H01723
[Journal Article] Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions2019
- Author(s)
  Tatsuta Makoto、Nakazawa Koji、Kimura Daisuke
- Journal Title
  
  LNCS (APLAS 2019)
  
  Volume: 11893 Pages: 367-387
- DOI
  10.1007/978-3-030-34175-6_19
- ISBN
  9783030341749, 9783030341756
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-18K11161, KAKENHI-PROJECT-17H01722
[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
[Presentation] ゲーデルのシステムTのための循環ラムダ計算2024
- Author(s)
  木村大輔, Stefano Berardi, Makoto Tatsuta, Ugo de'Ligoro, Koji Nakazawa
- Organizer
  MLG 59, 東北大学情報科学研究科
- Data Source
  KAKENHI-PROJECT-21H03421
[Presentation] 分離論理における記号ヒープのための循環証明体系におけるカットの制限について2020
- Author(s)
  早乙女献自，中澤巧爾，木村大輔
- Organizer
  第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)
- Data Source
  KAKENHI-PROJECT-18K11161
[Presentation] Failure of cut-elimination in cyclic proofs of separation logic2019
- Author(s)
  Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno
- Organizer
  第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019)
- Data Source
  KAKENHI-PROJECT-18K11161
[Presentation] On cut elimination in cyclic-proof systems2019
- Author(s)
  Koji Nakazawa, Daisuke Kimura, Tachio Terauchi, Hiroshi Unno, and Kenji Saotome
- Organizer
  3rd Workshop on Mathamatical Logic and Its Applications (MLA 2019)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-18K11161
[Presentation] Spatial factorization in cyclic-proof system for separation logic2019
- Author(s)
  Koji Nakazawa, Makoto Tatsuta, and Daisuke Kimura
- Organizer
  第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019)
- Data Source
  KAKENHI-PROJECT-18K11161
[Presentation] Decidability of Entailments in Separation Logic with Arrays2016
- Author(s)
  Daisuke Kimura
- Organizer
  Workshop on Mathematical Logic and its Application
- Place of Presentation
  京都大学
- Year and Date
  2016-09-16
- 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

1. Nakazawa Koji (80362581)

# of Collaborated Projects: 3 results

# of Collaborated Products: 10 results
2. Tatsuta Makoto (80216994)

# of Collaborated Projects: 2 results

# of Collaborated Products: 7 results

KIMURA Daisuke 木村 大輔

木村 大輔 キムラ ダイスケ

Research Projects

Research Products

Co-Researchers

循環証明体系の計算論的分析Principal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

循環証明体系におけるカット除去定理とカット規則の制限

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Development for software verification by separation logic

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Proof theoretic analysis of cyclic proof systems

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Theory of software verification by separation logic

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

[Journal Article] Restriction on cut rule in cyclic-proof system for symbolic heaps2024

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Cut-elimination for cyclic proof systems with inductively defined propositions2022

Author(s)

Journal Title

Data Source

[Journal Article] Biabduction for Separation Logic with Arrays and Lists2022

Author(s)

Journal Title

Data Source

[Journal Article] Decidability for Entailments of Symbolic Heaps with Arrays2021

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Function Pointer Eliminator for C Programs2021

Author(s)

Journal Title

DOI

ISBN

Data Source

[Journal Article] Restriction on Cut in Cyclic Proof System for Symbolic Heaps2020

Author(s)

Journal Title

DOI

ISBN

Data Source

[Journal Article] Failure of Cut-Elimination in Cyclic Proofs of Separation Logic2020

Author(s)

Journal Title

DOI

NAID

ISSN

Year and Date

Language

Data Source

[Journal Article] Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions2019

Author(s)

Journal Title

DOI

ISBN

Data Source

KIMURA Daisuke 木村大輔

木村大輔キムラダイスケ