Kenji Saotome, Koji Nakazawa, and Daisuke Kimura. Restriction on cut rule in cyclic-proof system for symbolic heaps. Theoretical Computer Science, 1019, December 2024. (Extended version of the precedent conference paper in FLOPS 2020.). [ DOI ]
Yeonseok Lee and Koji nakazawa. Relative completeness of incorrectness separation logic. In The 22nd Asian Symposium on Programming Languages and Systems (APLAS 2024), Kyoto, Japan, volume 15194 of Lecture Notes in Computer Science (LNCS), 2024. [ DOI ]
佐藤 拓海, 中澤 巧爾, and 木村 大輔. 分割可能なアクセス権限値をもつ並行分離論理における帰納的述語の拡張. In 第26回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2024), 2024.
Daisuke Kimura, Makoto Tatsuta, Mahmudul Faisal Al Ameen, Mirai Ikebuchi, and Koji Nakazawa. Bi-abduction in separation logic with arrays and lists for program analysis. Computer Software, 41:50--67, 2024. (Revised version of the proceeding in PPL2022.). [ DOI ]
Yeonseok Lee and Koji Nakazawa. Decidable entailment checking for concurrent separation logic with fractional permissions. Computer Software, 40, 2023. (Revised version of the proceeding in the 39th JSSST Annual Conference.). [ DOI ]
Koji Nakazawa, Ken-etsu Fujita, and Yuta Imagawa. Z property for shuffling calculus. Mathematical Structures in Computer Science, 23:1015--1027, August 2022. (Revised version of the precedent workshop paper in IWC2017.). [ DOI ]
Daisuke Kimura, Makoto Tatsuta, Mahmudul Faisal Al Ameen, Mirai Ikebuchi, and Koji Nakazawa. Biabduction for separation logic with arrays and lists. In 第24回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2022), 2022.
Daisuke Kimura, Mahmudul Faisal Al Ameen, Makoto Tatsuta, and Koji Nakazawa. Function pointer eliminator for C programs (tool paper). In 19th Asian Symposium on Programming Languages and Systems (APLAS), Chicago, US (online), volume 13008 of Lecture Notes in Computer Science (LNCS), pages 23--37, October 2021. [ DOI ]
Kenji Saotome, Koji Nakazawa, and Daisuke Kimura. Failure of cut-elimination in cyclic proofs of bunched logic with inductive propositions. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), Buenos Aires, Argentina (online), volume 195 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1--11:14, July 2021. [ DOI ]
Yuki Honda, Koji Nakazawa, and Ken-etsu Fujita. Confluence proofs of lambda-mu-calculi by Z theorem. Studia Logica, 109:917--936, 2021. [ DOI ]
Kenji Saotome, Koji Nakazawa, and Daisuke Kimura. Restriction on cut in cyclic proof system for symbolic heaps. In The 15th International Symposium on Functional and Logic Programming (FLOPS 2020), Akita, Japan (online), volume 12073 of Lecture Notes in Computer Science (LNCS), pages 88--105, September 2020. [ DOI ]
福井 康介, 中澤 巧爾, 石井 沙織, and 結縁 祥治. 古典論理に対する汎用的自然演繹の証明正規化. In 第22回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2020), 2020. （PPL2020論文賞）. [ .pdf ]
Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, and Mitsuru Yamamura. Spatial factorization in cyclic-proof system for separation logic. Computer Software, 37:125--144, 2020. (Revised version of the precedent workshop paper in PPL2019.) (JSSST Best Research Paper Award). [ DOI ]
Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno. Failure of cut-elimination in cyclic proofs of separation logic. Computer Software, 37:39--52, 2020. (Revised version of the precedent workshop paper in PPL2019.). [ DOI ]
Makoto Tatsuta, Koji Nakazawa, and Daisuke Kimura. Completeness of cyclic proofs for symbolic heaps with inductive definitions. In The 17th Asian Symposium on Programming Languages and Systems (APLAS 2019), Bali, Indonesia, volume 11893 of Lecture Notes in Computer Science (LNCS), pages 367--387, December 2019. [ DOI ]
Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, and Mitsuru Yamamura. Spatial factorization in cyclic-proof system for separation logic. In 第21回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2019), March 2019. [ .pdf ]
Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno. Failure of cut-elimination in cyclic proofs of separation logic. In 第21回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2019), March 2019. [ .pdf ]
Kosuke Fukui and Koji Nakazawa. Complete axiom system of cluster algebra. In 7th International Workshop on Cofluence (IWC 2018), Oxford, UK, July 2018. [ .pdf ]
井上 鉄也 and 中澤 巧爾. 高階契約に対するトレース意味論の完全抽象性. In 第20回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2018), March 2018. [ .pdf ]
Koji Nakazawa, Ken-etsu Fujita, and Yuta Imagawa. Z for call-by-value. In 6th International Workshop on Cofluence (IWC 2017), Oxford, UK, pages 57--61, September 2017. [ .pdf ]
Koji Nakazawa and Ken-etsu Fujita. Compositional Z: Confluence proofs for permutative conversion. Studia Logica, 104:1205--1224, December 2016. [ DOI ]
Takeshi Tsukada and Koji Nakazawa. Intersection and union type assignment and polarised lambda-bar-mu-mu-tild. In 第18回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2016), March 2016.
村井 涼, 五十嵐 淳, and 中澤 巧爾. 高階契約を持つプログラミング言語に対するトレース意味論. In 第17回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2015), March 2015.
Koji Nakazawa and Hiroto Naya. Strong reduction of combinatory logic with streams. Studia Logica, 103:375--387, April 2015. [ DOI ]
Koji Nakazawa and Tomoharu Nagai. Reduction system for extensional lambda-mu calculus. In 25th International Conference on Rewriting Techniques and Applications joint with the 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014), volume 8560 of Lecture Notes in Computer Science (LNCS), pages 340--363, July 2014. [ DOI ]
José Espírito Santo, Ralph Matthes, Koji Nakazawa, and Luís Pinto. Confluence for classical logic through the distinction between values and computation. In Paulo Oliva, editor, The Fifth International Workshop on Classical Logic and Computation (CL&C'14), volume 164 of Electric Proceedings in Theoretical Computer Science (EPTCS), pages 63--77, July 2014. [ DOI ]
José Espírito Santo, Ralph Matthes, Koji Nakazawa, and Luís Pinto. Monadic translation of classical sequent calculus. Mathematical Structures in Computer Science, 23:1111--1162, December 2013. [ DOI ]
Koji Nakazawa and Shin-ya Katsumata. Extensional models of untyped lambda-mu calculus. In Herman Geuvers and Ugo de'Liguoro, editors, Proceedings Fourth Workshop on Classical Logic and Computation (CL&C 2012), volume 97 of Electric Proceedings in Theoretical Computer Science (EPTCS), pages 35--47, October 2012. [ DOI ]
Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, and Hiroshi Nakano. Type checking and typability in domain-free lambda calculi. Theoretical Computer Science, 412(44):6193--6207, October 2011. (Extended version of the precedent conference paper in CSL2008.). [ DOI ]
Koji Nakazawa and Makoto Tatsuta. Type checking and inference for polymorphic and existential types in multiple-quantifier and type-free systems. Chicago Journal of Theoretical Computer Science, Special Issue: Selected papers from 2009 Computing: The Australasian Theory Symposium (CATS 2009), Article 7, 2010. (Jounal version of the precedent conference paper: Type Checking and Inference for Polymorphic and Existential Types, CATS 2009, Wellington, New Zealand, January, 2009.). [ .html ]
Yuki Kato and Koji Nakazawa. Type checking and inference are equivalent in lambda calculi with existential types. In Santiago Escobar, editor, 18th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2009), Revised Selected Papers, Brasilia, Brazil, volume 5979 of Lecture Notes in Computer Science (LNCS), pages 96--110. Springer, April 2010. [ DOI ]
Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, and Hiroshi Nakano. Undecidability of type-checking in domain-free typed lambda calculi with existence. In Michael Kaminski and Simone Martini, editors, Computer Science Logic (CSL 2008), Bertinoro, Italy, volume 5213 of Lecture Notes in Computer Science (LNCS), pages 478--492. Springer, September 2008. [ DOI ]
Koji Nakazawa and Makoto Tatsuta. Strong normalization of classical natural deduction with disjunctions. Annals of Pure and Applied Logic, 153:21--37, April 2008. [ DOI ]
Koji Nakazawa. An isomorphism between cut-elimination procedure and proof reduction. In Simona Ronchi Della Rocca, editor, Typed Lambda Calculi and Applications (TLCA2007), volume 4583 of Lecture Notes in Computer Science (LNCS), pages 336--350. Springer, 2007. [ DOI ]
Satoshi Ikeda and Koji Nakazawa. Strong normalization proofs by CPS-translations. Information Processing Letters, 99(4):163--170, August 2006. [ DOI ]
中澤 巧爾 and 龍田 真. 選言を含む自然演繹古典論理の強正規化性. In 第8回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2006), March 2006. (PPL2006 Best Paper Award). [ .pdf ]
池田 聡 and 中澤 巧爾. コントロールオペレータをもつ計算体系の強正規化可能性のCPS変換を用いた証明. In 第7回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2005), pages 171--186, March 2005. [ .pdf ]
Koji Nakazawa and Makoto Tatsuta. Strong normalization proof with CPS-translation for second order classical natural deduction. The Journal of Symbolic Logic, 68(3):851--859, September 2003. Corrigendum of this article is available in, The Journal of Symbolic Logic, 68(4):1415--1416, December 2003. (doi:10.2178/jsl/1067620196). [ DOI ]
Koji Nakazawa. Confluency and strong normalizability of call-by-value λμ-calculus. Theoretical Computer Science, 290:429--463, January 2003. [ DOI ]
佐藤 拓海 and 中澤 巧爾. 再帰呼び出しを含む分離論理の部分正当性のための循環証明体系. In 日本ソフトウェア科学会第41回大会講演論文集, September 2024.
Daisuke Kimura, Koji Nakazawa, and Kenji Saotome. Cut-elimination for cyclic proof systems with inductively defined propositions. In Theory and Applications of Proof and Computation, volume 2228 of RIMS Kokyuroku, pages 59--72, August 2022.
赤坂 陸来, 藤田 憲悦, and 中澤 巧爾. 合流性とZ定理について. In 証明と計算の理論と応用, volume 2228 of 数理解析研究所講究録, pages 30--40, August 2022.
Yeonseok Lee and Koji Nakazawa. Decidable entailment checking for concurrent separation logic with fractional permissions. In 日本ソフトウェア科学会第39回大会講演論文集, 2022. （優秀発表賞，学生奨励賞）.
本多 雄樹 and 中澤 巧爾. 書換え系の変換を用いたZ性の証明. In 日本ソフトウェア科学会第37回大会講演論文集, 2020.
Kousuke Fukui, Saori Ishii, Koji Nakazawa, and Takeshi Tsukada. Proof normalization for classical truth-table natural deduction. In 日本ソフトウェア科学会第37回大会講演論文集, 2020.
Makoto Tatsuta, Koji Nakazawa, and Daisuke Kimura. Completeness of cyclic proofs for symbolic heaps. arXiv.org, April 2018. [ https ]
Ken-etsu Fujita and Koji Nakazawa. Church-Rosser theorem and compositional Z-property. In 日本ソフトウェア科学会第33回大会講演論文集, September 2016. [ .pdf ]
仲田 壮佑 and 中澤 巧爾. 帰納的述語定義を含む分離論理における循環証明による半自動証明. In 日本ソフトウェア科学会第33回大会講演論文集, September 2016. [ .pdf ]
Koji Nakazawa and Ken-etsu Fujita. Compositional Z: Confluence proofs for permutative conversion. In 日本ソフトウェア科学会第32回大会講演論文集, September 2015. (高橋奨励賞). [ .pdf ]
Koji Nakazawa. Combinators for streams. In 日本ソフトウェア科学会第28回大会講演論文集, September 2011. [ .pdf ]
中澤 巧爾. 値呼びラムダ・ミュー計算の合流性と強正規化性. In 日本ソフトウェア科学会第17回大会講演論文集 (CD-ROM), September 2000. [ .pdf ]
Yeonseok Lee and Koji Nakazawa. Incorrectness separation logic with array and pointer arithmetic. 計算・言語・論理の研究集会 2024 御宿, September 2024.
佐藤 拓海 and 中澤 巧爾. 再帰呼び出しを含む分離論理の部分正当性のための循環証明体系. 計算・言語・論理の研究集会 2024 御宿, September 2024.
早乙女 献自 and 中澤 巧爾. 循環証明体系におけるカット規則の除去と制限. 計算・言語・論理の研究集会 2024 御宿, September 2024.
Koji Nakazawa and Yeonseok Lee. Relative completeness of incorrectness separation logic. SLACS 2024, 東北大学, August 2024.
堀 弘昌, 中澤 巧爾, and 龍田 真. 不動点演算子を持つ命題論理に対する循環証明体系のカット無し完全性. In 第26回プログラミングおよびプログラミング言語ワークショップ (PPL2024) ポスター，新潟, March 2024. [ .pdf ]
Lee Yeonseok and Koji Nakazawa. Toward completeness of incorrectness separation logic. In 第26回プログラミングおよびプログラミング言語ワークショップ (PPL2024) ポスター，新潟, March 2024. [ .pdf ]
女屋 優貴, 藤田 憲悦, and 中澤 巧爾. Z定理のモジュール性. 「証明論と計算論の最前線」，RIMS共同研究(公開型), 京都大学, December 2023.
中澤巧爾 and 早乙女献自. 循環証明とカット除去. 計算・言語・論理の研究集会 2023 御宿, August 2023.
堀弘昌 and 中澤巧爾. 無限証明体系と循環証明体系の証明能力同等性. 計算・言語・論理の研究集会 2023 御宿, August 2023.
中澤巧爾, 堀弘昌, and 龍田真. 不動点演算子を持つ命題論理の循環証明体系. SLACS 2022, 東邦大学, September 2022.
堀弘昌, 中澤巧爾, and 龍田真. 命題論理に対する無限証明体系と循環証明体系の証明能力同等性. In 日本数学会秋季総合分科会, 北海道大学, September 2022.
Yeonseok Lee and Koji Nakazawa. Normalization of symbolic heaps for entailment checking in concurrent separation logic with fractional permissions. In 第24回プログラミングおよびプログラミング言語ワークショップ (PPL2022) ポスター, online, March 2022. [ .pdf ]
堀弘昌, 中澤巧爾, and 龍田真. 無限証明体系と循環証明体系の証明能力同等性. In 第24回プログラミングおよびプログラミング言語ワークショップ (PPL2022) ポスター, online, March 2022. [ .pdf ]
石井沙織 and 中澤巧爾. 制限された帰納的述語を含む分離論理の完全な循環証明体系. In 第24回プログラミングおよびプログラミング言語ワークショップ (PPL2022) ポスター, online, March 2022. [ .pdf ]
中澤 巧爾, 早乙女 献自, and 木村 大輔. 帰納的命題を含む循環証明体系のカット除去. 「証明と計算の理論と応用」，RIMS共同研究(公開型), 京都大学, December 2021.
赤坂 陸来, 藤田 憲悦, and 中澤 巧爾. 合流性とZ定理について. 「証明と計算の理論と応用」，RIMS共同研究(公開型), 京都大学, December 2021.
中澤 巧爾. 分離論理. 数学基礎論サマースクール, online, September 2021.
Kenji Saotome, Koji Nakazawa, and Daisuke Kimura. Failure of cut-elimination in the cyclic proof system of bunched logic with inductive propositions. In The 4th Workshop on Mathamatical Logic and Its Applications, online, March 2021.
飯田 晟樹, 早乙女 献自, and 中澤 巧爾. 分離論理におけるエンテイルメント判定問題の決定不能性. In 第23回プログラミングおよびプログラミング言語ワークショップ (PPL2021) ポスター, online, March 2021. [ .pdf ]
早乙女 献自 and 中澤 巧爾. 分離論理の循環証明体系における帰納的述語の制限とカット除去. SLACS 2020, online, December 2020.
本多 雄樹 and 中澤 巧爾. 書換え系の変換を用いたZ性の証明. SLACS 2020, online, December 2020.
早乙女 献自, 中澤 巧爾, and 木村 大輔. 分離論理における記号ヒープのための循環証明体系におけるカットの制限について. In 第22回プログラミングおよびプログラミング言語ワークショップ (PPL2020) ポスター（現地開催中止）, March 2020. [ .pdf ]
青木 洸佑, 中澤 巧爾, and 木村 大輔. 分離論理におけるエンテイルメント証明器の入力に対する制限の緩和. In 第22回プログラミングおよびプログラミング言語ワークショップ (PPL2020) ポスター（現地開催中止）, March 2020. [ .pdf ]
本多 雄樹, 中澤 巧爾, and 藤田 憲悦. Confluence proof of lambda-mu-calculus by Z thorem. In RIMS共同研究「証明論とその周辺」，京都大学, December 2019.
福井 康介, 中澤 巧爾, and 石井 沙織. Proof normalization for classical truth-table natural deduction. In RIMS共同研究「証明論とその周辺」，京都大学, December 2019.
早乙女 献自, 中澤 巧爾, and 木村 大輔. On restricted cut-elimination for cyclic proof system for separation logic. In RIMS共同研究「証明論とその周辺」，京都大学, December 2019.
Koji Nakazawa, Kosuke Fukui, and Saori Ishii. Proof normalization for classical truth-table natural deduction. In The 2019 Joint Workshop on Formal Methods, Shanghai, China, December 2019.
Koji Nakazawa, Daisuke Kimura, Tachio Terauchi, Hiroshi Unno, and Kenji Saotome. On cut elimination in cyclic-proof systems. In The 51st TRS meeting, Sounkyo, Japan, September 2019.
Yuuki Honda, Koji Nakazawa, and Ken-etsu Fujita. Confluence proof of lambda-mu-calculus by Z theorem. In The 51st TRS meeting, Sounkyo, Japan, September 2019.
Koji Nakazawa, Daisuke Kimura, and Keiji Kita. Counterexample generation for symbolic-heap entailment checking. In 2019 SJTU-JAIST-NU Follow-Up Workshop on Formal Methods, Hokkaido, June 2019.
中澤 巧爾. プログラムの正しさを証明する---分離論理入門---. 日本数学会2019年度年会，特別講演，東工大, March 2019.
Koji Nakazawa, Daisuke Kimura, Tachio Terauchi, Hiroshi Unno, and Kenji Saotome. On cut elimination in cyclic-proof systems. In The 3rd Workshop on Mathamatical Logic and Its Applications, Nancy, France, March 2019.
Makoto Tatsuta, Koji Nakazawa, and Daisuke Kimura. Completeness of cyclic proofs for symbolic heaps with cone inductive definitions. In The 3rd Workshop on Mathamatical Logic and Its Applications, Nancy, France, March 2019.
Daisuke Kimura, Makoto Tatsuta, and Koji Nakazawa. Entailment checking procedure for symbolic heap using complete cyclic proof system. In The 3rd Workshop on Mathamatical Logic and Its Applications, Nancy, France, March 2019.
早乙女 献自 and 中澤 巧爾. 循環証明体系における準カット除去可能性について. In 第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019) ポスター， 花巻温泉, March 2019.
本多 雄樹, 中澤 巧爾, and 藤田 憲悦. Z定理を用いたλμ計算の合流性証明. In 第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019) ポスター， 花巻温泉, March 2019.
Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno, and Kenji Saotome. On cut elimination in cyclic-proof system for separation logic. The 12th Joint Workshop on Formal Methods, Shanghai, China, December 2018.
Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno. On cut elimination in cyclic-proof system for separation logic. 16th Asian Symposium on Programming Languages and Systems (APLAS 2018), Poster, Wellington, New Zealand, December 2018. [ .pdf ]
Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno. On cut elimination in cyclic-proof system for separation logic. 4th Workshop on New Ideas and Emerging Results (NIER 2018), Wellington, New Zealand, December 2018.
Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, and Mitsuru Yamamura. Cyclic theorem prover for separation logic by magic wand. In 1st Workshop on Automated Deduction for Separation Logics (ADSL 2018), Oxford, UK, July 2018. [ .pdf ]
Koji Nakazawa, Makoto Tatsuta, and Daisuke Kimura. Satisfiability checking for symbolic heaps with cell predicates. SJTU-JAIST-NU Follow-Up Workshop of Formal Methods, Kirishima, June 2018.
仲田 壮佑 and 中澤 巧爾. 帰納的述語を含む分離論理によるプログラム検証のための ループ不変式の導出. In 第20回プログラミングおよびプログラミング言語ワークショップ (PPL2018) ポスター， 皆生温泉, March 2018. [ .pdf ]
Koji Nakazawa, Ken-etsu Fujita, and Yuta Imagawa. Z for call-by-value. RIMS共同研究「証明論と証明活動」，京都大学, December 2017.
Koji Nakazawa, Ken-etsu Fujita, and Yuta Imagawa. Z for call-by-value. 10th NSFC-JSPS Joint Workshop on Formal Methods, Xian, China, November 2017.
Makoto Tatsuta, Daisuke Kimura, and Koji Nakazawa. Complete cyclic-proof system for separation logic with general inductive predicates. Analysis and Verification of Pointer Programs, No. 100 of NII Shonan Meeting, Shonan, October 2017.
Makoto Tatsuta, Daisuke Kimura, and Koji Nakazawa. Complete cyclic-proof system for separation logic with general inductive predicates. SLACS 2017, 千葉工業大学, August 2017.
中澤 巧爾 and 今川 雄太. Z for cbv. ラムダ計算と論理の早春セミナー, 草津, March 2017.
Makoto Tatsuta, Daisuke Kimrua, and Koji Nakazawa. Cyclic-proof-based decision procedure for symbolic heaps and inductive definitions. First NII Programming and Logic Workshop, NII, March 2017.
Makoto Tatsuta, Daisuke Kimrua, and Koji Nakazawa. Cyclic-proof-based decision procedure for symbolic heaps and inductive definitions. 2nd Workshop on New and Emerging Results in Programming Languages and Systems, Halong Bay, Vietnam, November 2016.
中澤 巧爾. Characterizing trees for lambda-mu terms. SLACS 2016, 名古屋大学, August 2016.
仲田 壮佑 and 中澤 巧爾. 帰納的述語定義を含む分離論理における循環証明による半自動証明. SLACS 2016, 名古屋大学, August 2016.
Koji Nakazawa. Characterizing trees for lambda-mu terms (extended abstract). In 8th International Workshop on Higher-Order Rewriting (HOR 2016), Porto, Portugal, June 2016. [ .pdf ]
中澤 巧爾 and 仲田 壮佑. Cyclic-proof search for separation logic with inductive predicates. ラムダ計算と論理の早春セミナー, 草津, March 2016.
Miyamoto, Y., Suenaga, K., and Nakazawa, K. A denotational semantics of a probabilistic stream-processing language. In Workshop on probabilistic programming semantics (PPS 2016), Poster, Florida, US, January 2016.
Koji Nakazawa. Lambda calculi and confluence from A to Z. 4th International Workshop on Confluence (IWC 2015), Invited Talk, Berlin, August 2015.
中澤 巧爾. Compositional Z: toward modular proofs of confluence. In ラムダ計算と論理の早春セミナー，草津, March 2015.
五十嵐 淳, 中澤 巧爾, 馬谷 誠二, 関山 太朗, 花田 裕一朗, 大元 武, 宮本 洋平, and 末永 幸平. 京都大学 teen racketeer 養成コース. In 第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015) ポスター，松山, March 2015.
中澤 巧爾 and 藤田 憲悦. 置換簡約を含むラムダ計算の合流性. In 第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015) ポスター，松山, March 2015. [ .pdf ]
Koji Nakazawa. Confluence for lambda calculi with permutative conversion. In 42nd TRS meeting，Harumi, Tokyo, February 2015.
Koji Nakazawa. Confluence for lambda calculi with permutative conversion. In 9th NII Type Theory Workshop，NII, Tokyo, January 2015.
中澤 巧爾. Confluence proofs for permutation. In ラムダ計算と論理の晩夏セミナー (2014LLS)，草津, September 2014.
Koji Nakazawa. Extensional models of typed lambda-mu calculus. In The Fifth International Workshop on Classical Logic and Computation (CL&C'14), Vienna, short paper, July 2014.
永井 智映，中澤 巧爾. 外延的Λμ計算の簡約体系. In 第16回プログラミングおよびプログラミング言語ワークショップ (PPL2014) ポスター，阿蘇, March 2014.
村井 涼，五十嵐 淳，中澤 巧爾. 契約つきモジュール計算のトレース意味論に向けて. In 第16回プログラミングおよびプログラミング言語ワークショップ (PPL2014) ポスター，阿蘇, March 2014.
中澤 巧爾. Confluence proofs by translations. ラムダ計算と論理の晩夏セミナー (2013LLS), 草津, September 2013.
中澤 巧爾. Extensional model of Lambda-mu calculus. 証明論研究集会 2013, 慶應義塾大学, August 2013.
Koji Nakazawa. Continuations and classical logic: using continuations as a tool for classical logic. ACM SIGPLAN Continuation Workshop (CW2011), invited talk, Tokyo, September 2011.
中澤 巧爾. Combinators for streams. SLACS 2011, 奈良女子大学, September 2011.
中澤 巧爾. Combinators for streams. ラムダ計算と論理の晩夏セミナー (2011LLS), 草津, August 2011.
中澤 巧爾. ラムダ計算とラムダミュー計算のモデル. ISTセミナー, 京都大学大学院情報学研究科知能情報学専攻, June 2011.
大里 陽一，五十嵐 淳，中澤 巧爾. 例外機構を持つ型付きラムダ計算におけるパラメトリシティ. In 第13回プログラミングおよびプログラミング言語ワークショップ (PPL2011) ポスター，札幌, March 2011.
加藤 祐輝，中澤 巧爾. 多相型と存在型に対する型検査問題の同値性. In 第13回プログラミングおよびプログラミング言語ワークショップ (PPL2011) ポスター，札幌, March 2011.
Koji Nakazawa. Monadic translation of classical sequent calculus. SLACS 2010, Sendai, September 2010. Collaborated work with José Espírito Santo, Ralph Matthes, and Luís Pinto.
Koji Nakazawa. Monadic translation of classical sequent calculus. MLG44, Hakone, May 2010. Collaborated work with José Espírito Santo, Ralph Matthes, and Luís Pinto.
山口 洋平，中澤 巧爾. 古典シークエント計算の強正規化可能性の構文論的証明. PPL2010 （ショートプレゼンテーション）, Kotohira, March 2010.
中澤 巧爾. Type checking and inference in domain-free type systems. Kusatsu Seminar 2009 on Lambda Calculus and Logics (LLK 2009), Kusatsu, March 2009.
加藤 祐輝，中澤 巧爾. 存在型に対する型検査問題と型推論問題の同値性. In 第11回プログラミングおよびプログラミング言語ワークショップ (PPL2009) ポスター，Takayama, March 2009.
中澤 巧爾. Type checking and inference for polymorphic and existential types. SLACS-ALGI 2008, Kagoshima, August 2008.
Koji Nakazawa. Strong cut-elimination and CPS-translations. In T. Kutsia and M. Marin, editors, Austria-Japan Workshop on Symbolic Computation and Software Verification, Linz, number 07-09 in RISC-Linz Report Series, pages 15--16, July 2007.
Koji Nakazawa. An isomorphism between cut-elimination procedure and proof reduction. SCORE Summer Workshop on Symbolic Computation and Software Verification, Fuji Susono, August-September 2007.
中澤 巧爾. A subsystem of sequent calculus isomorphic to natural deduction. SLACS 2006, Tokyo, September 2006.
Koji Nakazawa. SN proofs by CPS-translations. Kusatsu Seminar 2006 on Lambda Calculus and Logics, Kusatsu, March 2006.
中澤 巧爾，池田 聡. SN-proofs by CPS-translations. SLACS 2005, Tokyo, September 2005.
中澤 巧爾. λμ計算の強正規化性の証明について. SLACS 2001, Tokyo, September 2001.
龍田 真，中澤 巧爾. CPS変換による強正規化性の証明. PPL2000 （ショートプレゼンテーション）, Hamamatsu, March 2000.
中澤 巧爾. 値呼びλμ計算の合流性と強正規化性. 証明論研究会「証明論とその周辺」, Tokyo, January 2000.
Notice: The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.