Selected papers and slides of Naoki Kobayashi
Check also
DBLP database,
which provides a more exhaustive list of publications.
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.
Journal Papers
 Naoki Kobayashi,
"Inclusion Between the Frontier Language of a NonDeterministic Recursive Program Scheme
and the Dyck Language is Undecidable",
accepted for publication in Theoretical Computer Science, a special issue in memory of Maurice Nivat.
[paper]
 Naoki Kobayashi,
"Model Checking HigherOrder Programs",
Journal of the ACM, 60(3), Article No.20, June 2013.
[paper
This is the author's version of the work. It is posted here by permission of ACM
for your personal use. Not for redistribution. The definitive version is
available from
here.]
 Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara, Kazuya Yaguchi,
"Functional Programs as Compressed Data",
to appear in HigherOrder and Symbolic Computation, PEPM2012 special issue.
A short version appeared in Proceedings of PEPM 2012, pp.5362, 2012, ©ACM, 2012.
 Naoki Kobayashi and Luke Ong,
"Complexity of Model Checking Recursion Schemes for Fragments of the Modal MuCalculus",
Logical methods in Computer Science, 2011.
 Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii, "Environmental Bisimulations for HigherOrder Languages",
ACM Transactions on Programming Languages and Systems, 33(1), 2011.
 Naoki Kobayashi and Davide Sangiorgi, "A hybrid type system for lockfreedom of mobile processes",
ACM Transactions on Programming Languages and Systems, 32(5), 2010.
[paper © ACM, 2010.
This is the author's version of the work. It is posted here by permission of ACM
for your personal use. Not for redistribution. The definitive version is available from
here.]
 Hans Hüttel, Naoki Kobayashi, and Takashi Suto
"Undecidable Equivalences for Basic Parallel Processes,"
Information and Computation, 207(7):812829, 2009.
(paper)
 Koichi Kodama, Kohei Suenaga, and Naoki Kobayashi,
"Translation of Treeprocessing Programs into Streamprocessing Programs
based on Ordered Linear Type,"
Journal of Functional Programming, 18(3), pp.331371, 2008.
A preliminary summary appeared in
Proceedings of 2nd Asian Symposium on Programming Language and Systems (APLAS 2004),
Springer LNCS 3302, pp.4156, 2004.
(
abstract
)
(paper)
 Futoshi Iwama and Naoki Kobayashi,
"A New Type System for JVM Lock Primitives,"
to appear in New Generation Computing. A summary appeared in Proceedings of ASIAPEPM'02, pp.156168, ACM Press, 2002.
[
abstract
]
[full paper ]
 Naoki Kobayashi, Kohei Suenaga, and Lucian Wischik,
"Resource Usage Analysis for the PiCalculus,"
Logical methods in Computer Science, 2(3:4), pp.142, 2006.
A preliminary summary appeared in
Proceedings of VMCAI 2006, Springer LNCS 3855, pp.298312, 2006.
(
abstract and full version )
(short version© SpringerVerlag)

Naoki Kobayashi, "TypeBased Information Flow Analysis for the PiCalculus",
Acta Informatica, Vol. 42, No.45, pp.291347, 2005
(
abstract
)
(full version )
 Atsushi Igarashi and Naoki Kobayashi, "Resource Usage Analysis,"
ACM Transactions on Programming Languages and Systems, 27(2), pp.264313, 2005.
A summary appeared in Proceedings of POPL 2002, pp.331342, ACM Press, 2002.
(
abstract
)
(summary in POPL©2002 ACM)
(full paper©2004 ACM)

Atsushi Igarashi and Naoki Kobayashi, "A Generic Type System for the PiCalculus",
Theoretical Computer Science,
Vol 311/13, pp. 121163.
A summary appeared in Proceedings of POPL 2001, pp.128141.
(Full version (small corrections were made on April 14, 2009)©2003 Elsevier Science)
 Naoki Kobayashi and Keita Shirane,
"Typebased Information Flow Analysis for LowLevel Languages,"
Computer Software 20(2), Iwanami Press, pp.221, 2003 (in Japanese).
The English version appeared in informal proceedings of the 3rd Asian Workshop on
Programming Languages and Systems (APLAS'02).
(
Abstract
)
(Full paper (In Japanese) )
( Shorter version written in English )
 Naoki Kobayashi,
"A Type System for LockFree Processes,"
Information and Computation, vol. 177, pp.122159, 2002.
A preliminary version appeared in
Proceedings of TCS2000, Springer LNCS 1872, pp.365389,
under the title "Type Systems for Concurrent Processes: From DeadlockFreedom
to LivelockFreedom, TimeBoundedness."
( abstract)
( Full Paper ©2001 Academic Press)
 Atsushi Igarashi and Naoki Kobayashi,
"Type Reconstruction for Linear PiCalculus with I/O Subtyping,"
Information and Computation, 161, pp.144, 2000.
Preliminary summary appeared
as "Typebased analysis of communication for concurrent programming
languages" in Proceedings of International Static Analysis
Symposium (SAS'97), Springer LNCS 1302, pp.187201
(
abstract
)
( Full Paper )
(
Preliminary summary in SAS
)
 Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner,
"Linearity and the PiCalculus, "
ACM Transactions on Programming Languages
and Systems, 21(5), pp.914947, 1999. (Preliminary summary appeared in
Proceedings of ACM SIGACT/SIGPLAN Symposium on Principles
of Programming Languages (POPL'96), pp.358371, 1996)
(abstract)
(Full paper)
(Summary in POPL'96)

Naoki Kobayashi,"TypeBased Useless Variable Elimination,"
HigherOrder and Symbolic Computation, 14(23), pp.221260, 2001.
A preliminary summary appeared in Proceedings of ACM SIGPLAN Workshop on
Partial Evaluation and SemanticsBased Program Manipulation
(PEPM'00), pp.8493, 2000.
(abstract)
(summary in PEPM'00)
(full paper)
 Naoki Kobayashi,
"A Partially DeadlockFree Typed Process Calculus,"
ACM Transactions on Programming Languages and Systems, Vol. 20, No. 2, pp.436482, 1998.
A preliminary summary appeared in the Proceedings of Twelfth IEEE
Symposium on
Logic in Computer Science (LICS'97), pp128139.
( abstract
)( postscript )
 Naoki Kobayashi and Akinori Yonezawa, "Towards Foundations of Concurrent
ObjectOriented Programming  Types and Language Design,"
Theory and Practice of Object Systems, John Wiley & Sons,
1(4), 1995 (Preliminary summary appeared in Proceedings of
ACM OOPSLA94, pp.3145
as "TypeTheoretic Foundations for Concurrent ObjectOriented
Programming")
(abstract)
 Naoki Kobayashi and Akinori Yonezawa,
"Asynchronous Communication Model Based on Linear Logic,"
Journal of Formal Aspects of Computing, Vol.7, No.2,
pp.113149, SpringerVerlag, 1995
(abstract)
Conference Papers
 Ren Fukaishi, Naoki Kobayashi, and Ryosuke Sato,
"Productivity Verification for Functional Programs by Reduction to Termination Verification",
Proceedings of PEPM 2024.
[a long version]
 Ryo Mukai, Naoki Kobayashi, and Ryosuke Sato,
"Parameterized Recursive Refinement Types for Automated Program Verification",
Proceedings of SAS 2022.
[a long version]
 Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, and Hiroshi Unno,
"Temporal Verification of Programs via FirstOrder Fixpoint Logic",
Proceedings of SAS 2019.
[a long version]
 Naoki Kobayashi, Takeshi Tsukada, and Keiichi Watanabe,
"HigherOrder Program Verification via HFL Model Checking",
Proceedings of ESOP 2018.
[a long version]
 Adrien Champion, Tomoya Chiba, Naoki Kobayashi, and Ryosuke Sato,
"ICEbased Refinement Type Discovery for HigherOrder Functional Programs",
Proceedings of TACAS 2018. A revised and extended version was published in Journal of Automated Reasoning,
64(7), pp.13931418, 2020.
[a long version]
 Kazuyuki Asada and Naoki Kobayashi,
"Pumping Lemma for Higherorder Languages",
Proceedings of ICALP 2017.
[a long version]
 Naoki Kobayashi, Etienne Lozes, and Florian Bruse,
"On the Relationship between HigherOrder Recursion Schemes and HigherOrder Fixpoint Logic",
Proceedings of POPL 2017.
[the conference version© ACM].
[a longer version]
 Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, and Naoki Kobayashi,
"Predicate Abstraction and CEGAR for Disproving Termination of Higherorder Functional Programs",
Proceedings of CAV 2015.
© SpringerVerlag.
[longer version]
 Yuma Matsumoto, Naoki Kobayashi, and Hiroshi Unno,
"AutomataBased Abstraction for Automated Verification of HigherOrder TreeProcessing Programs",
Proceedings of APLAS 2015.
© SpringerVerlag.
[longer version]
 Naoki Kobayashi and Xin Li,
"AutomataBased Abstraction Refinement for muHORS Model Checking", Proceedings of LICS 2015.
[short version© IEEE]
[longer version]
 Taku Terao and Naoki Kobayashi,
"A ZDDbased Efficient HigherOrder Model Checking Algorithm",
Proceedings of APLAS 2014.
publisher version© SpringerVerlag.
authors' version.
[Note: There was an error in Table 1 of the publisher version.
The "D" column for the row "filternonzero1" should be "Y", instead of "N". See the authors' version.
]
 Elena Giachino, Naoki Kobayashi, and Cosimo Laneve,
"Deadlock analysis of unbounded process networks",
Proceedings of CONCUR 2014.
short version© SpringerVerlag.
[longer version]
 Kazuhide Yasukata, Naoki Kobayashi, and Kazutaka Matsuda,
"Pairwise Reachability Analysis for Higher Order Concurrent Programs by HigherOrder Model Checking",
Proceedings of CONCUR 2014.
short version© SpringerVerlag.
[longer version]
[Note: There was a flaw in the automata used in the experiments reported in the published version,
hence Table 1 of the published version is wrong. The corrected experimental result is
given in Table 1 of the longer version above.
]
 Naoki Kobayashi, Kazuhiro Inaba, and Takeshi Tsukada,
"Unsafe Order2 Tree Languages are ContextSensitive",
Proceedings of FoSSaCS 2014, 2014.
© SpringerVerlag.
[long version]
(Note: the short version that appeared in Proceedings of FoSSaCS 2014 contained a few errors,
which have been corrected in the long version)
 Christopher Broadbent and Naoki Kobayashi,
"SaturationBased Model Checking of HigherOrder Recursion Schemes", Proceedings of CSL 2013.
[paper]
 Naoki Kobayashi,
"Pumping by Typing", Proceedings of LICS 2013.
[short version© IEEE (This is a preliminary version.
The final version will be available from IEEE.)]
[longer version]
 Naoki Kobayashi and Atsushi Igarashi,
"Model Checking HigherOrder Programs with Recursive Types",
Proceedings of ESOP 2013, 2013.
© SpringerVerlag.
[PDF]
 Yoshihiro Tobita, Takeshi Tsukada and Naoki Kobayashi,
"Exact Flow Analysis by HigherOrder Model Checking."
Proceedings of FLOPS 2012, pp.275289, 2012
© SpringerVerlag.
[PDF]
[extended version]
 Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno,
"Predicate Abstraction and CEGAR for HigherOrder Model Checking",
To appear in Proceedings of PLDI 2011, 2011.
[paper © ACM, 2011.
This is the author's version of the work. It is posted here by permission of ACM
for your personal use. Not for redistribution. The definitive version will be published in Proceedings of PLDI 2011.]
 Naoki Kobayashi,
"A Practical Linear Time Algorithm for Trivial Automata Model Checking of HigherOrder Recursion Schemes",
A short version appears in Proceedings of FoSSaCS 2011.
[long version]

Morten Dahl, Naoki Kobayashi, Yunde Sun, and Hans Huttel,
"TypeBased Automated Verification of Authenticity in Asymmetric Cryptographic Protocols,"
Proceedings of ATVA 2011, Springer LNCS 6996, pp.7589, 2011.
[paper© Springer, 2011.]
 Naoki Kobayashi, Naoshi Tabuchi, and Hiroshi Unno,
"HigherOrder MultiParameter Tree Transducers and Recursion Schemes for
Program Verification",
Proceedings of POPL 2010, pp.495508, 2010.
[paper © ACM, 2010.
This is the author's version of the work. It is posted here by permission of ACM
for your personal use. Not for redistribution. The definitive version will be published in Proceedings of POPL'10.]
 Kohei Suenaga and Naoki Kobayashi,
"Fractional Ownerships for Safe Memory Deallocation."
To appear in APLAS 2009© SpringerVerlag.
[PDF]
 Naoki Kobayashi,
"ModelChecking HigherOrder Functions",
To appear in PPDP 2009.
[paper © ACM, 2009.
This is the author's version of the work. It is posted here by permission of ACM
for your personal use. Not for redistribution. The definitive version will be published in Proceedings of PPDP'09.]
 Naoki Kobayashi and Luke Ong,
"Complexity of Model Checking Recursion Schemes for Fragments of the Modal MuCalculus."
ICALP 2009© SpringerVerlag.
(superceded by the journal version)
 Naoki Kobayashi and Luke Ong,
"A Type System Equivalent to Modal MuCalculus Model Checking of Recursion Schemes,"
A revised version will appear in LICS 2009.
[preliminary version]
[a draft of the revised and extended version]
 Daisuke Kikuchi and Naoki Kobayashi,
"TypeBased Automated Verification of Autheticity in Cryptographic Protocols,"
Proceedings of ESOP 2009, Springer LNCS, 2009.
[paper© SpringerVerlag]
 Naoki Kobayashi,
"Types and HigherOrder Recursion Schemes for Verification of HigherOrder Programs,"
Proceedings of POPL 2009, pp.416428, 2009.
[paper© ACM, 2009.
This is the author's version of the work. It is posted here by permission of ACM
for your personal use. Not for redistribution. The definitive version was published in Proceedings of POPL'09.
http://doi.acm.org/10.1145/1480881.1480993.]
 Naoki Kobayashi and Davide Sangiorgi,
"A Hybrid Type System for LockFreedom of Mobile Processes,"
Proceedings of CAV 2008, Springer LNCS 5123, pp.8093, 2008.
 Naoki Kobayashi and Hitoshi Ohsaki,
"Tree Automata for NonLinear Arithmetic,"
Proceedings of RTA 2008, Springer LNCS 5117, pp.291305, 2008.
 Hiroshi Unno and Naoki Kobayashi,
"OnDemand Refinement of Dependent Types,"
Proceedings of FLOPS 2008, Springer LNCS 4989, pp.8196, 2008.
 Yuta Kaneko and Naoki Kobayashi,
"Linear Declassification,"
Proceedings of ESOP 2008, Springer LNCS 4960, pp.224238, 2008.
 Daisuke Kikuchi and Naoki Kobayashi,
"TypeBased Verification of Correspondence Assertions for Communication Protocols,"
Proceedings of APLAS 2007, Springer LNCS, to appear.
[
abstract
]
[paper© SpringerVerlag]
 Naoki Kobayashi and Takashi Suto,
"Undecidability of 2Label BPP Equivalences and Behavioral Type Systems for the PiCalculus,"
Proceedings of ICALP 2007, Springer LNCS 4596, pp.740751, 2007.
[
abstract
]
[short version© SpringerVerlag]
[full version]
[
Undecidability of BPP Equivalences Revisited
(a supplementary note on the flaws of Hans Huttel's proof of undecidability of
BPP equivalences and a corrected proof)]
 Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii,
"Environmental Bisimulations for HigherOrder Languages,"
LICS 2007, pp.303312, 2007.
[
abstract
]
[short version©2007 IEEE]
 Kohei Suenaga and Naoki Kobayashi,
"TypeBased Analysis of Deadlock for a Concurrent Calculus with Interrupts",
Proceedings of ESOP 2007, Springer LNCS 4421, pp.490504, 2007.
[short version© SpringerVerlag]
 Naoki Kobayashi,
"A New Type System for DeadlockFree Processes,"
Proceedings of CONCUR 2006, Springer LNCS 4137, pp.233247, 2006.
(
abstract
)
(short version© SpringerVerlag)
(full version)
 Hiroshi Unno, Naoki Kobayashi, and Akinori Yonezawa,
"Combining TypeBased Analysis and Model Checking for Finding
Counterexamples against NonInterference,"
Proceedings of ACM SIGPLAN Workshop on
Programming Languages and Analysis for Security (PLAS 2006),
pp.1726, 2006.
(abstract)
(paper©2006 ACM)
 Futoshi Iwama, Atsushi Igarashi and Naoki Kobayashi,
"Resource Usage Analysis for a Functional Language with Exceptions,"
Proceedings of ACM SIGPLAN 2006 Workshop on Partial Evaluation and Program Manipulation (PEPM 2006),
pp.3847, 2006.
(
abstract
)
(shorter version©2006 ACM)
 Kohei Suenaga, Naoki Kobayashi, and Akinori Yonezawa,
"Extension of TypeBased Approach to Generation of StreamProcessing
Programs by Automatic Insertion of Buffering Primitives,"
Proceedings of LOPSTR 2005, 2005.
(
abstract
)
(short version© SpringerVerlag)
 Akihito Nagata, Naoki Kobayashi, and Akinori Yonezawa,
"RegionBased Memory Management for a DynamicallyTyped Language,"
Proceedings of 2nd Asian Symposium on Programming Language and Systems (APLAS 2004),
Springer LNCS 3302, pp.229245, 2004.
(
abstract
)
(short version© SpringerVerlag)

Naoki Kobayashi, "UselessCode Elimination and Program Slicing for the PiCalculus",
Proceedings of
the First Asian Symposium on Programming Languages and Systems (APLAS'03),
Springer LNCS 2895, pp.5572.
(
abstract
)
(short version© SpringerVerlag)
(full version)

"Time Regions and Effects for Resource Usage Analysis"
(
abstract
)
(Summary ©2003 ACM)
(full paper )
 Naoki Kobayashi
 The summary appeared in
Proceedings of ACM SIGPLAN International Workshop on
Types in Languages Design and Implementation (TLDI'03), pp.5061, 2003.

"Type Systems for Concurrent Programs"
(
abstract
)
(paper© SpringerVerlag)
(extended version)
 Naoki Kobayashi
 Proceedings of
UNU/IIST 10th Anniversary Colloquium, LNCS 2757, pp.439453.

"An ImplicitlyTyped DeadlockFree Process Calculus"
(
abstract
) (Summary
©2000 Springer)
( Full Paper )
 Naoki Kobayashi, Shin Saito, and Eijiro Sumii
 A summary appeared in Proceedings of CONCUR2000.
A preliminary version of the full paper has been published as
Technical Report TR0001, Department of Information Science,
University of Tokyo, January 2000.

"QuasiLinear Types"
(abstract)
(summary in POPL'99)
(full version)
 Naoki Kobayashi
 A revised version of the paper published as
a technical report TR9802, Department of Information Science,
University of Tokyo, September 1998.
A summary appeared in the Proceedings of ACM POPL'99, pp.2942.

"A Generalized DeadlockFree Process Calculus"
( abstract
)(full version is available from
here )
 Eijiro Sumii and Naoki Kobayashi
 Summary will appear in Proceedings of Workshop on HighLevel Concurrent
Language (HLCL'98),
ENTCS, Vol.16, No.3.
Full version will appear as a technical report from
Department of Information Science, University of Tokyo
 "Static Analysis of Communication for Asynchronous Concurrent Programming Languages"
(abstract)
(postscript file)
 Naoki Kobayashi, Motoki Nakade, and Akinori Yonezawa
 Second International Static Analysis Symposium (SAS'95),
LNCS 983, pp.225242, 1995.
 "HigherOrder Concurrent Linear Logic Programming"
(abstract)
 Naoki Kobayashi and Akinori Yonezawa
 Theory and Practice of Parallel Programming, LNCS 907, pp.137166,
Springer Verlag, 1995.
 "PARCS: An MPPOriented CLP language"
 K. Konno, M. Nagatsuka, N. Kobayashi, S. Matsuoka, and A. Yonezawa
 Proceedings of the First
International Symposium on Parallel Symbolic Computation (PASCO'94),
pp.254263, World Scientific, September 1994.
 "ACL  A Concurrent Linear Logic Programming Paradigm"
 Naoki Kobayashi and Akinori Yonezawa
 Logic Programming: Proceedings of the 1993 International
Symposium, pp.279294, MIT Press, 1993.
Slides and Videos for Talks
 "An Overview of the HFL Model Checking Project":
Video ,
Slides
 Naoki Kobayashi
 Invited Talk at HCVS 21
 "10 Years of the HigherOrder Model Checking Project":
Video ,
Slides
 Naoki Kobayashi
 Invited Talk at PPDP 2019 and LOPSTR 2019
 PPL 2018 tutorial on HORS/HFL model checking (in Japanese):
Slides
 POPL 2016 tutorial: "HigherOrder Model Checking"
See this page

"Towards a Software Model Checker for ML"
(Slides)
 Naoki Kobayashi
 Invited Talk at ML Workshop 2011

"HigherOrder Model Checking: From Theory to Practice"
(Slides)
 Naoki Kobayashi
 Invited Talk at LICS 2011

"Types and Recursion Schemes for HigherOrder Program Verification"
(Part 1)(Part 2)
 Naoki Kobayashi
 Presented at Workshop on HigherOrder Recursion Schemes and Pushdown Automata

"Types and HigherOrder Recursion Schemes for HigherOrder Program Verification"
Slides
 Naoki Kobayashi
 Invited talk at APLAS 2009
 Note: See also the slides above presented at
Workshop on HigherOrder Recursion Schemes and Pushdown Automata, which contain
more technical details.

"Substructural Type Systems for Program Analysis"
(Slides)
 Naoki Kobayashi
 Invited Talk at FLOPS 2008, April 1416, Ise, Japan.

"Type Systems for Concurrent Programs"
(Slides)
Back to the Home Page