Presentations -
-
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 International coauthorship
Yeonseok Lee, Koji Nakazawa
2022.8.31
-
Normalization of symbolic heaps for entailment checking in concurrent separation logic with fractional permissions International coauthorship
2022.3.6
-
無限証明体系と循環証明体系の証明能力同等性 International coauthorship
堀弘昌，中澤巧爾，龍田真
第24回プログラミングおよびプログラミング言語ワークショップ (PPL2022) 2022.3.7 日本ソフトウェア科学会プログラミング論研究会
-
制限された帰納的述語を含む分離論理の完全な循環証明体系 International coauthorship
石井沙織，中澤巧爾
第24回プログラミングおよびプログラミング言語ワークショップ (PPL2022) 2022.3.7 日本ソフトウェア科学会プログラミング論研究会
-
帰納的命題を含む循環証明体系のカット除去
中澤巧爾，早乙女献自，木村大輔
RIMS共同研究「証明と計算の理論と応用」 2021.12.20
-
合流性とZ定理について
赤坂陸来，藤田憲悦，中澤巧爾
RIMS共同研究「証明と計算の理論と応用」 2021.12.20
-
分離論理 Invited
中澤 巧爾
2021年度数学基礎論サマースクール（古典論理に限らない論理） 2021.9 日本数学会
-
Failure of cut-elimination in the cyclic proof system of bunched logic with inductive propositions International conference
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 International conference
Koji Nakazawa, Daisuke Kimura, Tachio Terauchi, Hiroshi Unno, Kenji Saotome
The 51st TRS Meeting
-
Confluence Proof of lambda-mu-Calculus by Z Theorem International conference
Yuuki Honda, Koji Nakazawa, Ken-etsu Fujita
The 51st TRS Meeting
-
プログラムの正しさを証明する ---分離論理入門--- Invited
中澤 巧爾
日本数学会2019年度年会
-
Z定理を用いたラムダ・ミュー計算の合流性証明
本多 雄樹, 中澤 巧爾
第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019)
-
循環証明体系における準カット除去可能性について
早乙女 献自, 中澤 巧爾
第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019)
-
On Cut-Elimination in Cyclic Proof Systems International conference
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 International conference
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. International conference
Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, Mitsuru Yamamura
1st Workshop on Automated Deduction for Separation Logics (ADSL 2018)
-
Complete Axiom System of Cluster Algebra International conference
Kousuke Fukui and Koji Nakazawa
7th International Workshop on Confluence (IWC 2018)
-
帰納的述語を含む分離論理によるプログラム検証のための ループ不変式の導出
仲田 壮佑, 中澤 巧爾
第20回プログラミングおよびプログラミング言語ワークショップ (PPL2018)
-
Completeness of Cyclic Proofs for Symbolic Heaps. International conference
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 Invited International conference
-
Cyclic-Proof-Based Decision Procedure for Symbolic Heaps and Inductive Definitions International conference
Makoto Tatsuta, Daisuke Kimura, Koji Nakazawa
2nd Workshop on New and Emerging Results in Programming Languages and Systems
-
Characterizing trees for lambda-mu terms International conference
Koji Nakazawa
8th International Workshop on Higher-Order Rewriting (HOR 2016)
-
A denotational semantics of a probabilistic stream-processing language International conference
Yohei Miyamoto, Kohei Suenaga, Koji Nakazawa
Workshop on probabilistic programming semantics (PPS 2016)
-
Lambda calculi and confluence from A to Z International conference
K. Nakazawa
4th International Workshop on Confluence (IWC 2015)
-
置換簡約を含むラムダ計算の合流性
中澤巧爾, 藤田憲悦
第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015)
-
京都大学 teen racketeer 養成コース
五十嵐 淳, 中澤 巧爾, 馬谷 誠二, 関山 太朗, 花田 裕一朗, 大元 武, 宮本 洋平, 末永 幸平
第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015)
-
Extensional models of typed lambda-mu calculus International conference
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 International conference
K. Nakazawa
Continuation Workshop (CW2011)