List of Publications by Koji Nakazawa
[English][dblp]
Last Update:
Tue Aug 11 15:36:26 JST 2015
Papers
- Koji Nakazawa and Hiroto
Naya.
Strong reduction of combinatory logic with streams.
Studia Logica, 103:375–387, April 2015.
(doi:10.1007/s11225-014-9570-3)
- 村井 涼,
五十嵐 淳, and 中澤 巧爾.
高階契約を持つプログラミング言語に対するトレース意味論.
In 第17回プログラミングおよびプログラミング言語ワークショップ論文集
(PPL2015), March 2015.
- 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, pages
63–77, July 2014.
(doi:10.4204/EPTCS.164.5)
- 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, pages 340–363, July 2014.
(doi:10.1007/978-3-319-08918-8_24)
- 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:10.1017/S0960129512000436)
- 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, pages 35–47, October 2012.
(doi:10.4204/EPTCS.97.3)
- 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:10.1016/j.tcs.2011.06.020)
- Koji
Nakazawa.
Combinators for streams.
In 日本ソフトウェア科学会第28回大会講演論文集 (CD-ROM), September
2011.
(Errata).
(PDF)
- 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.).
(PDF)
- 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, pages 96–110. Springer, April 2010.
(doi:10.1007/978-3-642-11999-6_7)
- 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, pages 478–492. Springer,
September 2008.
(doi:10.1007/978-3-540-87531-4_34)
- 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:10.1016/j.apal.2008.01.003)
- 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, pages 336–350. Springer, 2007.
(doi:10.1007/978-3-540-73228-0_24)
- Satoshi Ikeda and Koji
Nakazawa.
Strong normalization proofs by CPS-translations.
Information Processing Letters, 99(4):163–170, August 2006.
(doi:10.1016/j.ipl.2006.03.009)
- 中澤 巧爾 and 龍田 真.
選言を含む自然演繹古典論理の強正規化性.
In 第8回プログラミングおよびプログラミング言語ワークショップ論文集
(PPL2006), March 2006.
(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:10.2178/jsl/1058448444)
- Koji
Nakazawa.
Confluency and strong normalizability of call-by-value λμ-calculus.
Theoretical Computer Science, 290:429–463, January 2003.
(doi:10.1016/S0304-3975(01)00380-2)
- 中澤
巧爾.
値呼びラムダ・ミュー計算の合流性と強正規化性.
In 日本ソフトウェア科学会第17回大会講演論文集 (CD-ROM), September
2000.
(PDF)
Talks and Others
- 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 藤田 憲悦.
置換簡約を含むラムダ計算の合流性.
In 第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015)
ポスター,松山, March 2015.
- 五十嵐 淳, 中澤 巧爾,
馬谷 誠二, 関山 太朗, 花田
裕一朗, 大元 武, 宮本 洋平, and
末永 幸平.
京都大学 teen racketeer 養成コース.
In 第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015)
ポスター,松山, March 2015.
- 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.
- 加藤 祐輝,中澤 巧爾.
存在型に対する型検査問題と型推論問題の同値性.
In 第11回プログラミングおよびプログラミング言語ワークショップ (PPL2009)
ポスター,Takayama, March 2009.
- 中澤
巧爾.
Type checking and inference in domain-free type systems.
Kusatsu Seminar 2009 on Lambda Calculus and Logics (LLK 2009), Kusatsu, March
2009.
- 中澤
巧爾.
Type checking and inference for polymorphic and existential types.
SLACS-ALGI 2008, Kagoshima, August 2008.
- 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.
- 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.
- 中澤
巧爾.
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.
[HOME]