木村 大輔

Bi-Abduction in Separation Logic with Arrays and Lists for Program Analysis 

コンピュータソフトウェア 41(1) 50-67 2024年1月  査読有り筆頭著者責任著者

Coqによる三角形三色問題の証明 

コンピュータソフトウェア 40(3) 2-15 2023年8月  査読有り責任著者

Extending a Call-by-Value Calculus Based on Bilateralism with Dynamic Binding 

Journal of Applied Logics 10(4) 511-530 2023年7月  査読有り招待有り

A typed lambda-calculus with first-class configurations 

Journal of Logic and Computation (exac062) 2022年10月  査読有り

Cut-Elimination for Cyclic Proof Systems with Inductively Defined Propositions 

数理解析研究所講究録 2228 59-72 2022年8月  筆頭著者責任著者

Biabduction for Separation Logic with Arrays and Lists 

第24回プログラミングおよびプログラミング言語ワークショップ (PPL2022) 2022年3月  査読有り筆頭著者責任著者

A study for recovering the cut-elimination property in cyclic proof systems by restricting the arity of inductive predicates 

第24回プログラミングおよびプログラミング言語ワークショップ (PPL2022) 2022年3月  査読有り責任著者

Function Pointer Eliminator for C Programs 

The 19th Asian Symposium on Programming Languages and Systems (APLAS 2021) 2021年  査読有り筆頭著者責任著者

Failure of Cut-elimination in Cyclic Proofs of Bunched Logic with Inductive Propositions. 

The 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), Leibniz International Proceedings in Informatics (LIPIcs) 195 11:1-11:14 2021年  査読有り

A Symmetric Lambda-Calculus Corresponding to the Negation-Free Bilateral Natural Deduction. 

CoRR abs/2101.12607 2021年  責任著者

Decidability for Entailments of Symbolic Heaps with Arrays. 

Logical Methods in Computer Science 17(2) 2021年  査読有り筆頭著者責任著者

Restriction on Cut in Cyclic Proof System for Symbolic Heaps 

Functional and Logic Programming (FLOPS 2020), LNCS 12073 88-105 2020年  査読有り

Spatial Factorization in Cyclic-Proof System for Separation Logic 

コンピュータ ソフトウェア 37(1) 125-144 2020年  査読有り

Failure of Cut-Elimination in Cyclic Proofs of Separation Logic 

コンピュータ ソフトウェア 37(1) 39-52 2020年  査読有り筆頭著者責任著者

Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions. 

Proceedings of The 17th Asian Symposium on Programming Languages and Systems (APLAS2019) 367-387 2019年  査読有り

Cyclic Theorem Prover for Separation Logic by Magic Wand 

In First Workshop on Automated Deduction for Separation Logics (ADSL) at FLoC 2018年7月  査読有り

Decidability of Entailments in Separation Logic with Arrays and Lists 

第 20 回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2018) 2018年3月  査読有り筆頭著者責任著者

Completeness of Cyclic Proofs for Symbolic Heaps. 

CoRR abs/1804.03938 2018年  査読有り

Decision Procedure for Entailment of Symbolic Heaps with Arrays. 

Proceedings of the 15th Asian Symposium on Programming Languages and Systems (APLAS2017), Lecture Notes in Computer Science 10695 169-189 2017年  査読有り筆頭著者責任著者

Translation of Symbolic Heaps with Monadic Inductive Definitions into Monadic Second-Order Logic 

第 18 回プログラミングおよびプログラ ミング言語ワークショップ論文集 (PPL2016) 2016年3月  査読有り

Separation Logic with Monadic Inductive Definitions and Implicit Existentials. 

Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS2015), LNCS 9458 69-89 2015年  査読有り

Induction by Coinduction and Control Operators in Call-by-Name. 

Proceedings of COS'13 workshop EPTCS 127 101-112 2013年  査読有り責任著者

Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types 

Logical Methods in Computer Science 9(1) 2013年  査読有り筆頭著者責任著者

Dual Calculus with Inductive and Coinductive Types. 

Rewriting Techniques and Applications (RTA 2009) 5595 224-238 2009年  査読有り筆頭著者責任著者

Classical Natural Deduction for S4 Modal Logic. 

New Generation Computing 29(1) 243-258 2009年  査読有り筆頭著者責任著者

古典S4様相論理に対応する計算系 

2009年  査読有り筆頭著者責任著者

Computation in Classical Logic and Dual Calculus. 

2007年  査読有り筆頭著者責任著者