龍田 真

J-GLOBALへ         更新日: 17/04/27 20:25
 
アバター
研究者氏名
龍田 真
URL
http://research.nii.ac.jp/~tatsuta
所属
国立情報学研究所
職名
教授
学位
東京大学博士(理学)

研究分野

 
 

受賞

 
2017年4月
European Association for Theoretical Computer Science (EATCS) EATCS Award for ETAPS best paper 受賞
 
2006年3月
日本ソフトウェア科学会 Best Paper Award受賞
受賞者: 中澤 巧爾、龍田 真
 
1990年1月
日本ソフトウェア科学会 高橋奨励賞
受賞者: 龍田 真、小林 聡
 

論文

 
A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic
Proceedings of 29th International Conference on Computer-Aided Verification (CAV2017)      2017年7月   [査読有り]
Equivalence of Inductive Definitions and Cyclic Proofs under Arithmetic
Proceedings of Thirty-Second Annual IEEE Symposium on Logic in Computer Science (LICS2017)      2017年6月   [査読有り]
Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proof System
Lecture Notes in Computer Science      2017年4月   [査読有り]
Decision Procedure for Symbolic Heaps with Arrays
Proceedings of the 18th JSSST Workshop on Programming and Programming Languages (PPL2017)      2017年3月   [査読有り]
Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
Lecture Notes in Computer Science   10017 1-21   2016年11月   [査読有り]
Translation of Symbolic Heaps with Monadic Inductive Definitions into Monadic Second-Order Logic
Proceedings of the 18th JSSST Workshop on Programming and Programming Languages (PPL2016)   1-15   2016年3月   [査読有り]
Completeness for Recursive Procedures in Separation Logic
Theoretical Computer Science      2016年   [査読有り]
Separation Logic with Monadic Inductive Definitions and Implicit Existentials
Lecture Notes in Computer Science   9458 69-89   2015年11月   [査読有り]
Completeness of Separation Logic with Inductive Definitions for Program Verification,
Makoto Tatsuta and Wei-Ngan Chin
Lecture Notes in Computer Science   8702 20-34   2014年9月   [査読有り]
BERARDI Stefano
Lecture Notes in Computer Science   7941 61-76   2013年6月   [査読有り]
Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types
Logical Methods in Computer Science   9(1) Article 14   2013年1月   [査読有り]
Internal Models of System F for Decompilation
Theoretical Computer Science   435 3-20   2012年6月   [査読有り]
Verification of Substitution Theorem Using HOL
Information Processing Society of Japan Transactions on Programming   5(2) 88-96   2012年3月   [査読有り]
Non-Commutative Infinitary Peano Arithmetic
Leibniz International Proceedings in Informatics   12 538-552   2011年9月   [査読有り]
Type Inference for Bimorphic Recursion
Electronic Proceedings in Theoretical Computer Science   102-115   2011年6月   [査読有り]
NAKAZAWA Koji
Theoretical Computer Science   412(44) 6193-6207   2011年3月   [査読有り]
Wontae Choi, Baris Aktemur, Kwangkeun Yi, and Makoto Tatsuta
Proceedings of 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages   46(1) 81-92   2011年1月   [査読有り]
分離論理によるポインタープログラム検証の完全性
龍田 真, Wei-Ngan Chin, Mahmudul Faisal Al Ameen
日本ソフトウェア科学会第27回大会      2010年9月
On Isomorphisms of Intersection Types (共著)
Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti and Makoto Tatsuta
ACM Transactions on Computational Logic   11(4) Article 25   2010年7月   [査読有り]
Inhabitation of Polymorphic and Existential Types
Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa, and Hiroshi Nakano
Annals of Pure and Applied Logic   161(11) 1390-1399   2010年6月   [査読有り]
Internal Normalization, Compilation and Decompilation for System F
Stefano Berardi and Makoto Tatsuta
Lecture Notes in Computer Science   6009 207-223   2010年4月   [査読有り]
Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems
Koji Nakazawa and Makoto Tatsuta
Chicago Journal of Theoretical Computer Science   Article 7   2010年4月   [査読有り]
Completeness of Pointer Program Verification by Separation Logic
M. Tatsuta, W.N. Chin, and M.F. Al Ameen
Proceeding of 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2009)   179-188   2009年11月   [査読有り]
Non-Commutative First-Order Sequent Calculus
Makoto Tatsuta
Proceedings of 18th EACSL Annual Conference on Computer Science Logic (CSL2009), Lecture Notes in Computer Science   5771 470-484   2009年9月   [査読有り]
Dual Calculus with Inductive and Coinductive Types (共著)
Daisuke Kimura and Makoto Tatsuta
Proceedings of 20th International Conference on Rewriting Techniques and Applications (RTA 09), Lecture Notes in Computer Science   5595 224-238   2009年6月   [査読有り]
Type Checking and Inference for Polymorphic and Existential Types (共著)
Koji Nakazawa and Makoto Tatsuta
Proceedings of The 15th Computing: The Australasian Theory Symposium (CATS2009), Conferences in Research and Practice in Information Technology   94 61-69   2009年1月   [査読有り]
Second-Order Logic without Implication nor Disjunction
Makoto Tatsuta
Proceedings of 10th Asian Logic Conference (ALC 10), Bulletin of Symbolic Logic      2008年9月   [査読有り]
Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence (共著)
Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, and Hiroshi Nakano
Proceedings of 17th EACSL Annual Conference on Computer Science Logic (CSL2008), Lecture Notes in Computer Science   5213 478-492   2008年9月   [査読有り]
On Isomorphisms of Intersection Types (共著)
Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, Makoto Tatsuta
Proceedings of 17th EACSL Annual Conference on Computer Science Logic (CSL2008), Lecture Notes in Computer Science   5213 461-477   2008年9月   [査読有り]
遺伝的置換子の型とTLCA未解決問題20番
龍田 真
日本ソフトウェア科学会第25回大会論文集      2008年9月
Inhabitance of Existential Types is Decidable in Negation-Product Fragment (共著)
Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa, and Hiroshi Nakano
Proceedings of 2nd International Workshop on Classical Logic and Computation (CLC2008)      2008年7月   [査読有り]
Types for Hereditary Permutators
Makoto Tatsuta
Proceedings of Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS2008)   83-92   2008年6月   [査読有り]
Some Non-Recursively-Enumerable Sets and Their Types
Makoto Tatsuta
Proceedings of Workshop on Constructivism: Logic and Mathematics      2008年5月   [招待有り]
Strong normalization of classical natural deduction with disjunctions
Koji Nakazawa, Makoto Tatsuta
Annals of Pure and Applied Logic      2008年4月   [査読有り]
Types for Hereditary Head Normalizing Terms
Makoto Tatsuta
Proceedings of Ninth International Symposium on Functional and Logic Programming (FLOPS 2008), Lecture Notes in Computer Science   4989 195-209   2008年4月   [査読有り]
Positive Arithmetic without Exchange is a Subclassical Logic
Stefano Berardi, Makoto Tatsuta
Lecture Notes in Computer Science   4807 271-285   2007年11月   [査読有り]
Types for Hereditary Permutators
Makoto Tatsuta
NII Technical Report      2007年11月
Simple saturated sets for disjunction and second-order existential quantification (to appear)
Makoto Tatsuta
Lecture Notes in Computer Science   4583 366-380   2007年6月   [査読有り]
The maximum length of mu-reduction in lambda mu-calculus (to appear)
Makoto Tatsuta
Lecture Notes in Computer Science   4533 359-373   2007年6月   [査読有り]
Uniqueness of D-normal Proofs
Makoto Tatsuta
NII Technical Report   (NII-20)    2006年12月
代入定理と永続強正規化可能性
龍田 真, マリアンジェラ・デザニ
日本ソフトウェア科学会第23回全国大会論文集   1-6   2006年9月
Normalisation is Insensible to lambda-term Identity or Difference, lambda-term Identity or Difference
Makoto Tatsuta and Mariangiola Dezani-Ciancaglini
Proceedings of Twenty First Annual IEEE Symposium on Logic in Computer Science   327-336   2006年8月   [査読有り]
選言を含む自然演繹古典論理の強正規化性
中澤巧爾, 龍田真
第8回プログラミングおよびプログラミング言語ワークショップ   187-202   2006年3月   [査読有り]
A Behavioural Model for Klop's Calculus
Mariangiola Dezani-Ciancaglini and Makoto Tatsuta
Proceedings of Logic, Model and Computer Science 2006, Electronic Notes in Theoretical Computer Science 169   19-32   2006年3月   [査読有り]
Normalisation is Insensible to lambda-term Identity or Difference
Makoto Tatsuta and Mariangiola Dezani-Ciancaglini
NII Technical Report   (NII-20)    2006年3月
M. Tatsuta
Progress in Informatics   (2) 41-56   2005年12月   [査読有り]
置換簡約をもつ二階自然演繹の強正規化可能性
龍田 真, G. Mints
2005年度日本数学会年会アブストラクト      2005年3月
A Simple Proof of Second Order Strong Normalization with Permutative Conversions
M. Tatsuta and G. Mints
Annals of Pure and Applied Logic   136(39449) 134-155   2004年12月   [査読有り]
Strong Normalization Proof with CPS-Translation for Second Order Classical Natural Deduction
K. Nakazawa and M. Tatsuta
Journal Symbolic of Logic   68(3) 851-859   2003年9月   [査読有り]
CPS変換による強正規化性の証明
龍田 真, 中澤 巧
Second JSSST workshop on Programming and Programming Languages      2000年9月   [査読有り]
Long D-normal form yields uniqueness of proofs
S. Hirokawa and M. Tatsuta
Proceedings of 2000 European Congress of Association for Symbolic Logic      2000年8月   [査読有り]
構成的集合論の実現可能性とそのプログラム合成への応用
龍田 真
Proceedings of First JSSST workshop on Programming and Programming Languages   139-143   1999年9月
Uniqueness of D-normal Proofs
M. Tatsuta
Proceedings of 7th Asian Logic Conference   41-42   1999年6月   [査読有り]
構成的集合の実現可能性解釈
龍田 真
日本ソフトウェア科学会第15回大会論文集   189-192   1998年9月
構成的論理とプログラム理論
龍田 真
1998年度日本数学会秋季総合分科会総合講演企画特別講演アブストラクト (特別講演)   13-24   1998年9月   [招待有り]
Realizability of Monotone Coinductive Definitions and Its Application to Program Synthesis
M. Tatsuta
Proceedings of Fourth International Conference on Mathematics of Program Construction, LNCS 1422   338-364   1998年6月   [査読有り]
Realizability for Constructive Theory of Functions and Classes and Its Application to Program Synthesis
M. Tatsuta
Proceedings of Thirteenth Annual IEEE Symposium on Logic in Computer Science   358-367   1998年6月   [査読有り]
Uniform Continuity of Graph Model and Partial Function Model
M. Tatsuta
Proceedings of 1997-98 Annual Meeting of Association for Symbolic Logic   20-21   1998年5月   [査読有り]
The Function [a/m] in Sharply Bounded Arithmetic
M. Tada and M. Tatsuta
Archive for Mathematical Logic   37 51-57   1997年7月   [査読有り]
S. Kobayashi and M. Tatsuta
Theoretical Computer Science   131(1) 121-138   1994年8月   [査読有り]
M. Tatsuta
International Journal of Foundations of Computer Science   5(1) 1-21   1994年6月   [査読有り]
M. Tatsuta
Theoretical Computer Science   122(1/2) 119-136   1994年1月   [査読有り]
Uniqueness of Normal Proofs of Minimal Formulas
M. Tatsuta
Journal of Symbolic Logic   58(3) 789-799   1993年9月   [査読有り]
Realizability of Inductive Definitions for Constructive Programming (Doctoral Dissertation)
Makoto Tatsuta
博士論文      1993年3月   [査読有り]
Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams
M. Tatsuta
Proceedings of International Conference on Fifth Generation Computer Systems   666-673   1992年6月   [査読有り]
M. Tatsuta
Theoretical Computer Science   90(2) 309-353   1991年12月   [査読有り]
Monotone Recursive Definition of Predicates and Its Realizability Interpretation
M. Tatsuta
Proceedings of International Conference on Theoretical Aspects of Computer Software, LNCS 526   526 38-52   1991年9月   [査読有り]
直観主義的帰納的定義に対する実現可能性解釈
小林 聡, 龍田 真
ソフトウェア科学会第6回全国大会論文集   113-116   1989年10月

Misc

 
型理論 IV
龍田 真
コンピュータソフトェア 8 (4) 56--68      1991年7月
型理論 III
龍田 真
コンピュータソフトェア 8 (3) 2--8      1991年5月
型理論 II
龍田 真
コンピュータソフトェア 8 (2) 40--46      1991年3月
型理論 I
龍田 真
コンピュータソフトェア 8 (1) 25--33      1991年1月
書評: J.Y. Girard et al 著 Proofs and Types ( Cambridge Univ Press, 1989)
龍田 真
情報処理学会誌 1990      1990年8月

書籍等出版物

 
岩波数学辞典第4版
日本数学会編
岩波書店   2002年12月   
新版情報処理ハンドブック
情報処理学会編
オーム社   1995年11月   
型理論
龍田 真
近代科学社   1992年11月   

講演・口頭発表等

 
Cyclic-Proof-Based Decision Procedure for Symbolic Heaps and Inductive Definitions
2nd Workshop on New and Emerging Results in Programming Languages and Systems   2016年11月24日   
Decidable subsystem of Presburger Arithmetic with Inductive Definitions and Application to Symbolic Heaps
龍田 真
International Workshop on Mathematics for Computation (M4C)   2016年5月8日   
Decidability and Undecidability in Symbolic-Heap System with Inductive Definitions
Proceedings of Continuity, Computability, Constructivity: From Logic to Algorithms (CCC2015)   2015年9月16日   
Realizability of inductive and coinductive definitions [招待有り]
龍田 真
JAIST Logic Workshop Series 2015: Constructivism and Computability   2015年3月3日   
New complete system of Hoare's logic with recursive procedures
JAIST Logic Workshop Series 2015: Constructivism and Computability   2015年3月3日   
Verification of Substitution Theorem Using HOL
小合敬之, 龍田 真
第86回情報処理学会プログラミング研究会   2011年11月   
Infinite reductions are insensible to lambda-term identity or difference
Mariangiola Dezani and Makoto Tatsuta
Infinity Symposium, March 21--22, 2006, Vrije Universiteit Amsterdam   2006年3月21日   
Different Substitution Theorem
Makoto Tatsuta and Mariangiola Dezani-Ciancaglini
Workshop on Linear Logic, Proof Theory and Computer Science, March 16--17, 2006, Keio University   2006年3月16日   
Martin-Lof's type theory with permutative reductions
M. Tatsuta
Stanford Logic Seminar   2004年5月18日   
A simple proof of strong normalization with permutative conversions
M. Tatsuta and G. Mints
Stanford Logic Seminar   2004年2月3日   

Works

 
Proof Figure Macros proof.sty
M. Tatsuta   その他   1990年10月
http://research.nii.ac.jp/~tatsuta/proof-sty.html (1990).