中澤 巧爾

J-GLOBALへ         更新日: 18/12/08 05:04
 
アバター
研究者氏名
中澤 巧爾
 
ナカザワ コウジ
eメール
knaki.nagoya-u.ac.jp
URL
http://www.sqlab.i.is.nagoya-u.ac.jp/~nakazawa/
所属
名古屋大学
部署
大学院情報学研究科  情報システム学専攻 ソフトウェア論
職名
准教授
学位
博士(理学)(京都大学)
科研費研究者番号
80362581

研究分野

 
 

経歴

 
2002年12月
 - 
2007年3月
京都大学大学院情報学研究科助手
 
2007年4月
 - 
2015年9月
京都大学大学院情報学研究科助教
 
2015年10月
 - 
2017年3月
名古屋大学 大学院情報科学研究科 情報システム学専攻 ソフトウェア論/工学部 准教授
 
2015年10月
 - 
現在
名古屋大学大学院情報科学研究科准教授
 
2017年4月
 - 
現在
名古屋大学 大学院情報学研究科  情報システム学専攻 ソフトウェア論 准教授
 

受賞

 
2016年9月
日本ソフトウェア科学会 高橋奨励賞
 

論文

 
Studia Logica   104 1205-1224   2016年12月   [査読有り]
Studia Logica   103 375-387   2015年4月   [査読有り]
Strong normalization proof with CPS-translation for second order classical natural deduction
68(3) 851-859   2003年9月   [査読有り]
Koji Nakazawa
Mathematical Structures in Computer Science, to appear      2003年   [査読有り]

Misc

 
高階契約に対するトレース意味論の完全抽象性
井上 鉄也, 中澤 巧爾
第20回プログラミングおよびプログラミング言語ワークショップ(PPL2018)論文集   .   2018年3月   [査読有り]
Z for call-by-value
Koji Nakazawa, Ken-etsu Fujita, Yuta Imagawa
6th International Workshop on Cofluence (IWC 2017),   57–61   2017年9月   [査読有り]
Church-Rosser theorem and compositional Z-property
Ken-etsu Fujita, Koji Nakazawa
日本ソフトウェア科学会第33回大会講演論文集   .   2016年9月
帰納的述語定義を含む分離論理における循環証明による半自動証明
仲田 壮佑, 中澤 巧爾
日本ソフトウェア科学会第33回大会講演論文集   .   2016年9月
Koji Nakazawa, Ken-etsu Fujita
Studia Logica      2016年5月   [査読有り]

講演・口頭発表等

 
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)   2018年7月   
Complete Axiom System of Cluster Algebra
Kousuke Fukui and Koji Nakazawa
7th International Workshop on Confluence (IWC 2018)   2018年7月   
帰納的述語を含む分離論理によるプログラム検証のための ループ不変式の導出
仲田 壮佑, 中澤 巧爾
第20回プログラミングおよびプログラミング言語ワークショップ (PPL2018)   2018年3月5日   
Completeness of Cyclic Proofs for Symbolic Heaps.
Makoto Tatsuta, Koji Nakazawa, and Daisuke Kimura
Second Workshop on Mathematical Logic and its Applications (MLA 2018)   2018年3月   
Complete cyclic-proof system for separation logic with general inductive predicates [招待有り]
Makoto Tatsuta, Daisuke Kimura, Koji Nakazawa
Analysis and Verification of Pointer Programs, No. 100 of NII Shonan Meeting   2017年10月   
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   2016年11月24日   
Characterizing trees for lambda-mu terms
Koji Nakazawa
8th International Workshop on Higher-Order Rewriting (HOR 2016)   2016年6月25日   
A denotational semantics of a probabilistic stream-processing language
Yohei Miyamoto, Kohei Suenaga, Koji Nakazawa
Workshop on probabilistic programming semantics (PPS 2016)   2016年1月   
Lambda calculi and confluence from A to Z
K. Nakazawa
4th International Workshop on Confluence (IWC 2015)   2015年8月   
置換簡約を含むラムダ計算の合流性
中澤巧爾, 藤田憲悦
第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015)   2015年3月   
京都大学 teen racketeer 養成コース
五十嵐 淳, 中澤 巧爾, 馬谷 誠二, 関山 太朗, 花田 裕一朗, 大元 武, 宮本 洋平, 末永 幸平
第17回プログラミングおよびプログラミング言語ワークショップ (PPL2015)   2015年3月   
Extensional models of typed lambda-mu calculus
K. Nakazawa
The Fifth International Workshop on Classical Logic and Computation (CL&C'14)   2014年7月   
Extensional model of Lambda-mu calculus
中澤巧爾
証明論研究集会   2013年9月   
Continuations and classical logic: using continuations as a tool for classical logic
K. Nakazawa
Continuation Workshop (CW2011)   2011年9月   ACM SIGPLAN

担当経験のある科目

 
 

競争的資金等の研究課題

 
計算における無限概念と古典論理
日本学術振興会: 科学研究費助成事業
研究期間: 2015年4月 - 2018年3月    代表者: 中澤巧爾
ソフトウェア契約に基づく高階型付プログラムの理論
日本学術振興会: 科学研究費助成事業
研究期間: 2013年4月 - 2016年3月    代表者: 五十嵐淳
ストリーム計算のための計算モデル
日本学術振興会: 科学研究費助成事業
研究期間: 2012年4月 - 2015年3月    代表者: 中澤巧爾
バグのないソフトウェア構築環境に関する研究の新展開
日本学術振興会: 科学研究費助成事業
研究期間: 2010年4月 - 2013年3月    代表者: 佐藤雅彦
二階存在量化子をもつ計算体系
日本学術振興会: 科学研究費助成事業
研究期間: 2009年4月 - 2012年3月    代表者: 中澤巧爾

学歴

 
1994年4月
 - 
1998年3月
京都大学 理学部 
 
2000年4月
 - 
2002年11月
京都大学 理学研究科 数学・数理解析