講演・口頭発表等 - 中澤 巧爾
-
Incorrectness Separation Logic with Arrays and Pointer Arithmetic
Yeonseok Lee and Koji Nakazawa
2025年3月27日
-
再帰呼び出しを含む分離論理の部分正当性のための循環証明体系
佐藤拓海，中澤巧爾
第27回プログラミングおよびプログラミング言語ワークショップ (PPL2025) 2025年3月 日本ソフトウェア科学会プログラミング論研究会
-
Cyclic-proof systems for symbolic heaps require cut formulas outside initial signatures
Kenji Saotome and Koji Nakazawa
2025年1月14日
-
Relative completeness of incorrectness separation logic
Koji Nakazawa and Yeonseok Lee
2024年8月
-
Toward completeness of incorrectness separation logic
Lee Yeonseok and Koji Nakazawa
2024年3月
-
不動点演算子を持つ命題論理に対する循環証明体系のカット無し完全性
堀 弘昌, 中澤 巧爾, and 龍田 真
第26回プログラミングおよびプログラミング言語ワークショップ (PPL2024) 2024年3月 日本ソフトウェア科学会プログラミング論研究会
-
Z定理のモジュール性
女屋優貴，藤田憲悦，中澤巧爾
RIMS共同研究「証明論と計算論の最前線」 2023年12月11日
-
命題論理に対する無限証明体系と循環証明体系の証明能力同等性
堀弘昌, 中澤巧爾, 龍田真
日本数学会秋季総合分科会 2022年9月 日本数学会
-
不動点演算子を持つ命題論理の循環証明体系
中澤巧爾, 堀弘昌, 龍田真
SLACS 2022 2022年9月
-
Decidable entailment checking for concurrent separation logic with fractional permissions 国際共著
Yeonseok Lee, Koji Nakazawa
2022年8月31日
-
Normalization of symbolic heaps for entailment checking in concurrent separation logic with fractional permissions 国際共著
2022年3月6日
-
無限証明体系と循環証明体系の証明能力同等性 国際共著
堀弘昌，中澤巧爾，龍田真
第24回プログラミングおよびプログラミング言語ワークショップ (PPL2022) 2022年3月7日 日本ソフトウェア科学会プログラミング論研究会
-
制限された帰納的述語を含む分離論理の完全な循環証明体系 国際共著
石井沙織，中澤巧爾
第24回プログラミングおよびプログラミング言語ワークショップ (PPL2022) 2022年3月7日 日本ソフトウェア科学会プログラミング論研究会
-
帰納的命題を含む循環証明体系のカット除去
中澤巧爾，早乙女献自，木村大輔
RIMS共同研究「証明と計算の理論と応用」 2021年12月20日
-
合流性とZ定理について
赤坂陸来，藤田憲悦，中澤巧爾
RIMS共同研究「証明と計算の理論と応用」 2021年12月20日
-
分離論理 招待有り
中澤 巧爾
2021年度数学基礎論サマースクール（古典論理に限らない論理） 2021年9月 日本数学会
-
Failure of cut-elimination in the cyclic proof system of bunched logic with inductive propositions 国際会議
Koji Nakazawa, Kenji Saotome, Daisuke Kimura
Forth Workshop on Mathematical Logic and its Applications (MLA 2021) 2021年3月
-
分離論理におけるエンテイルメント判定問題の決定不能性
飯田 晟樹，早乙女 献自，中澤 巧爾
第23回プログラミングおよびプログラミング言語ワークショップ (PPL2021) 日本ソフトウェア科学会プログラミング論研究会
-
分離論理の循環証明体系における帰納的述語の制限とカット除去
早乙女 献自, 中澤 巧爾
SLACS 2020 2020年12月
-
書換え系の変換を用いたZ性の証明
本多 雄樹, 中澤 巧爾
SLACS 2020 2020年12月
-
書換え系の変換を用いたZ性の証明
本多 雄樹，中澤 巧爾
日本ソフトウェア科学会第 37 回大会 2020年9月 日本ソフトウェア科学会
-
Proof Normalization for Classical Truth-Table Natural Deduction
Kosuke Fukui, Saori Ishii, Koji Nakazawa, and Takeshi Tsukada
2020年9月
-
分離論理におけるエンテイルメント証明器の入力に対する制限の緩和
青木 洸佑, 中澤 巧爾, 木村 大輔
第22回プログラミングおよびプログラミング言語ワークショップ (PPL2020) 日本ソフトウェア科学会プログラミング論研究会
-
分離論理における記号ヒープのための循環証明体系におけるカットの制限について
早乙女 献自, 中澤 巧爾, 木村 大輔
第22回プログラミングおよびプログラミング言語ワークショップ (PPL2020) 日本ソフトウェア科学会プログラミング論研究会
-
On restricted cut-elimination for cyclic proof system for separation logic
-
Confluence proof of lambda-mu-calculus by Z thorem
-
Proof normalization for classical truth-table natural deduction
-
On cut elimination in cyclic-proof systems 国際会議
Koji Nakazawa, Daisuke Kimura, Tachio Terauchi, Hiroshi Unno, Kenji Saotome
The 51st TRS Meeting
-
Confluence Proof of lambda-mu-Calculus by Z Theorem 国際会議
Yuuki Honda, Koji Nakazawa, Ken-etsu Fujita
The 51st TRS Meeting
-
プログラムの正しさを証明する ---分離論理入門--- 招待有り
中澤 巧爾
日本数学会2019年度年会
-
Z定理を用いたラムダ・ミュー計算の合流性証明
本多 雄樹, 中澤 巧爾
第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019)
-
循環証明体系における準カット除去可能性について
早乙女 献自, 中澤 巧爾
第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019)
-
On Cut-Elimination in Cyclic Proof Systems 国際会議
Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno
16th Asian Symposium on Programming Languages and Systems (APLAS 2018)
-
On Cut-Elimination in Cyclic Proof Systems 国際会議
Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno
Workshop on New Ideas and Emerging Results (NIER 2019)
-
Cyclic Theorem Prover for Separation Logic by Magic Wand. 国際会議
Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, Mitsuru Yamamura
1st Workshop on Automated Deduction for Separation Logics (ADSL 2018)
-
Complete Axiom System of Cluster Algebra 国際会議
Kousuke Fukui and Koji Nakazawa
7th International Workshop on Confluence (IWC 2018)
-
帰納的述語を含む分離論理によるプログラム検証のための ループ不変式の導出
仲田 壮佑, 中澤 巧爾
第20回プログラミングおよびプログラミング言語ワークショップ (PPL2018)
-
Completeness of Cyclic Proofs for Symbolic Heaps. 国際会議
Makoto Tatsuta, Koji Nakazawa, and Daisuke Kimura
Second Workshop on Mathematical Logic and its Applications (MLA 2018)
-
Complete cyclic-proof system for separation logic with general inductive predicates 招待有り 国際会議
-
Cyclic-Proof-Based Decision Procedure for Symbolic Heaps and Inductive Definitions 国際会議
Makoto Tatsuta, Daisuke Kimura, Koji Nakazawa
2nd Workshop on New and Emerging Results in Programming Languages and Systems
-
Characterizing trees for lambda-mu terms 国際会議
Koji Nakazawa
8th International Workshop on Higher-Order Rewriting (HOR 2016)
-
A denotational semantics of a probabilistic stream-processing language 国際会議
Yohei Miyamoto, Kohei Suenaga, Koji Nakazawa
Workshop on probabilistic programming semantics (PPS 2016)
-
Lambda calculi and confluence from A to Z 国際会議
K. Nakazawa
4th International Workshop on Confluence (IWC 2015)
-
置換簡約を含むラムダ計算の合流性
中澤巧爾, 藤田憲悦
第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015)
-
京都大学 teen racketeer 養成コース
五十嵐 淳, 中澤 巧爾, 馬谷 誠二, 関山 太朗, 花田 裕一朗, 大元 武, 宮本 洋平, 末永 幸平
第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015)
-
Extensional models of typed lambda-mu calculus 国際会議
K. Nakazawa
The Fifth International Workshop on Classical Logic and Computation (CL&C'14)
-
Extensional model of Lambda-mu calculus
-
Continuations and classical logic: using continuations as a tool for classical logic 国際会議
K. Nakazawa
Continuation Workshop (CW2011)