default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDNaoki Kobayashi 0001
Person information
- affiliation: Graduate School of Information Science and Technology, University of Tokyo, Japan
Other persons with the same name
- Naoki Kobayashi — disambiguation page
- Naoki Kobayashi 0002 — NTT East Corporation Research and Development Center, Tokyo, Japan
- Naoki Kobayashi 0003 — Yamagata University School of Medicine, Japan
- Naoki Kobayashi 0004 — Toshiba Corporation
- Naoki Kobayashi 0005 — Hiroshima University, Japan
- Naoki Kobayashi 0006 — Tokyo University of Science, Japan
- Naoki Kobayashi 0007 — Tokyo Denki University, Dept. of Inf. Syst. & Multimedia Design
- Naoki Kobayashi 0008 — Keio University, Yokohama, Department of Electrical Engineering
- Naoki Kobayashi 0009 — Saitma Medical University, Hidaka-shi, Japan
- Naoki Kobayashi 0010 — Mie University, Tsu-city, Japan
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[j38]Mahmudul Faisal Al Ameen
, Naoki Kobayashi, Ryosuke Sato:
Asynchronous unfold/fold transformation for fixpoint logic. Sci. Comput. Program. 231: 103014 (2024)- [c139]Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato:
Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem. APLAS 2024: 325-345 - [c138]Ren Fukaishi, Naoki Kobayashi, Ryosuke Sato:
Productivity Verification for Functional Programs by Reduction to Termination Verification. PEPM 2024: 70-82 - [c137]Izumi Tanaka, Ken Sakayori, Naoki Kobayashi:
Ownership Types for Verification of Programs with Pointer Arithmetic. PEPM 2024: 94-106 - [c136]Takashi Nakayama, Yusuke Matsushita, Ken Sakayori, Ryosuke Sato, Naoki Kobayashi:
Borrowable Fractional Ownership Types for Verification. VMCAI (2) 2024: 224-246 - [e11]Naoki Kobayashi, James Worrell:
Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I. Lecture Notes in Computer Science 14574, Springer 2024, ISBN 978-3-031-57227-2 [contents] - [e10]Naoki Kobayashi, James Worrell:
Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part II. Lecture Notes in Computer Science 14575, Springer 2024, ISBN 978-3-031-57230-2 [contents] - 2023
- [j37]Hiroyuki Katsura, Naoki Kobayashi, Ryosuke Sato:
Higher-Order Property-Directed Reachability. Proc. ACM Program. Lang. 7(ICFP): 48-77 (2023) - [j36]Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, Takeshi Tsukada:
HFL(Z) Validity Checking for Automated Program Verification. Proc. ACM Program. Lang. 7(POPL): 154-184 (2023) - [c135]Ryo Ikeda, Ryosuke Sato, Naoki Kobayashi:
Argument Reduction of Constrained Horn Clauses Using Equality Constraints. APLAS 2023: 246-265 - [c134]Momoko Hattori, Naoki Kobayashi, Ryosuke Sato:
Gradual Tensor Shape Checking. ESOP 2023: 197-224 - [c133]Naoki Kobayashi, Minchao Wu:
Neural Network-Guided Synthesis of Recursive List Functions. TACAS (1) 2023: 227-245 - [i23]Takashi Nakayama, Yusuke Matsushita, Ken Sakayori, Ryosuke Sato, Naoki Kobayashi:
Borrowable Fractional Ownership Types for Verification. CoRR abs/2310.20430 (2023) - [i22]Izumi Tanaka, Ken Sakayori, Naoki Kobayashi:
Ownership Types for Verification of Programs with Pointer Arithmetic. CoRR abs/2312.06455 (2023) - 2022
- [c132]Mahmudul Faisal Al Ameen, Naoki Kobayashi, Ryosuke Sato:
Asynchronous Unfold/Fold Transformation for Fixpoint Logic. FLOPS 2022: 39-56 - [c131]Kazuyuki Asada, Hiroyuki Katsura, Naoki Kobayashi:
On Higher-Order Reachability Games Vs May Reachability. RP 2022: 108-124 - [c130]Ryoya Mukai, Naoki Kobayashi, Ryosuke Sato:
Parameterized Recursive Refinement Types for Automated Program Verification. SAS 2022: 397-421 - [i21]Kento Tanahashi, Naoki Kobayashi, Ryosuke Sato:
Automatic HFL(Z) Validity Checking for Program Verification. CoRR abs/2203.07601 (2022) - [i20]Momoko Hattori, Naoki Kobayashi, Ryosuke Sato:
Gradual Tensor Shape Checking. CoRR abs/2203.08402 (2022) - [i19]Kazuyuki Asada, Hiroyuki Katsura, Naoki Kobayashi:
On Higher-Order Reachability Games vs May Reachability. CoRR abs/2203.08416 (2022) - 2021
- [j35]Yo Mitani, Naoki Kobayashi, Takeshi Tsukada:
A Probabilistic Higher-order Fixpoint Logic. Log. Methods Comput. Sci. 17(4) (2021) - [j34]Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi:
RustHorn: CHC-based Verification for Rust Programs. ACM Trans. Program. Lang. Syst. 43(4): 15:1-15:54 (2021) - [c129]Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada:
Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination. APLAS 2021: 265-284 - [c128]Patrick Baillot, Alexis Ghyselen, Naoki Kobayashi:
Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes. CONCUR 2021: 34:1-34:22 - [c127]Mayuko Kori, Takeshi Tsukada, Naoki Kobayashi:
A Cyclic Proof System for HFL_ℕ. CSL 2021: 29:1-29:22 - [c126]Ryuta Kambe, Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara, Ryo Yoshinaka:
Inside-Outside Algorithm for Macro Grammars. ICGI 2021: 32-46 - [c125]Hideto Ueno, John Toman, Naoki Kobayashi, Takeshi Tsukada:
Counterexample generation for program verification based on ownership refinement types. PEPM@POPL 2021: 44-57 - [c124]Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno:
Toward Neural-Network-Guided Program Synthesis and Verification. SAS 2021: 236-260 - [c123]Takumi Shimoda, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato:
Symbolic Automatic Relations and Their Applications to SMT and CHC Solving. SAS 2021: 405-428 - [c122]Naoki Kobayashi:
An Overview of the HFL Model Checking Project. HCVS@ETAPS 2021: 1-12 - [e9]Naoki Kobayashi:
6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference). LIPIcs 195, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2021, ISBN 978-3-95977-191-7 [contents] - [d1]Takumi Shimoda, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato:
Symbolic Automatic Relations and Their Applications to SMT and CHC Solving. Zenodo, 2021
- [i18]Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno:
Toward Neural-Network-Guided Program Synthesis and Verification. CoRR abs/2103.09414 (2021) - [i17]Patrick Baillot, Alexis Ghyselen, Naoki Kobayashi:
Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes. CoRR abs/2104.07293 (2021) - [i16]Takumi Shimoda, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato:
Symbolic Automatic Relations and Their Applications to SMT and CHC Solving. CoRR abs/2108.07642 (2021) - [i15]Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada:
Termination Analysis for the π-Calculus by Reduction to Sequential Program Termination. CoRR abs/2109.00311 (2021) - 2020
- [j33]Adrien Champion, Tomoya Chiba, Naoki Kobayashi, Ryosuke Sato:
ICE-Based Refinement Type Discovery for Higher-Order Functional Programs. J. Autom. Reason. 64(7): 1393-1418 (2020) - [j32]Naoki Kobayashi, Ugo Dal Lago, Charles Grellois:
On the Termination Problem for Probabilistic Higher-Order Recursive Programs. Log. Methods Comput. Sci. 16(4) (2020) - [c121]Hiroyuki Katsura, Naoki Iwayama, Naoki Kobayashi, Takeshi Tsukada:
A New Refinement Type System for Automated $\nu \text {HFL}_\mathbb {Z}$ Validity Checking. APLAS 2020: 86-104 - [c120]Hiroaki Naganuma, Diptarama Hendrian, Ryo Yoshinaka, Ayumi Shinohara, Naoki Kobayashi:
Grammar Compression with Probabilistic Context-Free Grammar. DCC 2020: 386 - [c119]Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi:
RustHorn: CHC-Based Verification for Rust Programs. ESOP 2020: 484-514 - [c118]John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, Naoki Kobayashi:
ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs. ESOP 2020: 684-714 - [c117]Yo Mitani, Naoki Kobayashi, Takeshi Tsukada:
A Probabilistic Higher-Order Fixpoint Logic. FSCD 2020: 19:1-19:22 - [c116]Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada:
On Average-Case Hardness of Higher-Order Model Checking. FSCD 2020: 21:1-21:23 - [c115]Kazuyuki Asada, Naoki Kobayashi:
Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars. FSCD 2020: 22:1-22:22 - [c114]Naoki Iwayama, Naoki Kobayashi, Ryota Suzuki, Takeshi Tsukada:
Predicate Abstraction and CEGAR for $\nu \mathrm {HFL}_\mathbb {Z}$ Validity Checking. SAS 2020: 134-155 - [c113]Naoki Kobayashi, Grigory Fedyukovich, Aarti Gupta:
Fold/Unfold Transformations for Fixpoint Logic. TACAS (2) 2020: 195-214 - [e8]Holger Hermanns, Lijun Zhang, Naoki Kobayashi, Dale Miller:
LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020. ACM 2020, ISBN 978-1-4503-7104-9 [contents] - [i14]John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, Naoki Kobayashi:
ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs. CoRR abs/2002.07770 (2020) - [i13]Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi:
RustHorn: CHC-based Verification for Rust Programs (full version). CoRR abs/2002.09002 (2020) - [i12]Hiroaki Naganuma, Diptarama Hendrian, Ryo Yoshinaka, Ayumi Shinohara, Naoki Kobayashi:
Grammar compression with probabilistic context-free grammar. CoRR abs/2003.08097 (2020) - [i11]Mayuko Kori, Takeshi Tsukada, Naoki Kobayashi:
A Cyclic Proof System for HFLN. CoRR abs/2010.14891 (2020) - [i10]Yo Mitani, Naoki Kobayashi, Takeshi Tsukada:
A Probabilistic Higher-order Fixpoint Logic. CoRR abs/2011.14303 (2020)
2010 – 2019
- 2019
- [j31]Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada:
Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence. Log. Methods Comput. Sci. 15(1) (2019) - [j30]Naoki Kobayashi:
Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable. Theor. Comput. Sci. 777: 409-416 (2019) - [c112]Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada:
A Type-Based HFL Model Checking Algorithm. APLAS 2019: 136-155 - [c111]Naoki Kobayashi, Ugo Dal Lago, Charles Grellois:
On the Termination Problem for Probabilistic Higher-Order Recursive Programs. LICS 2019: 1-14 - [c110]Keiichi Watanabe, Takeshi Tsukada, Hiroki Oshikawa, Naoki Kobayashi:
Reduction from branching-time property verification of higher-order programs to HFL validity checking. PEPM@POPL 2019: 22-34 - [c109]Ryosuke Sato, Naoki Iwayama, Naoki Kobayashi:
Combining higher-order model checking with refinement type inference. PEPM@POPL 2019: 47-53 - [c108]Naoki Kobayashi:
10 Years of the Higher-Order Model Checking Project (Extended Abstract). PPDP 2019: 2:1-2:2 - [c107]Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, Hiroshi Unno:
Temporal Verification of Programs via First-Order Fixpoint Logic. SAS 2019: 413-436 - [c106]Yuya Okuyama, Takeshi Tsukada, Naoki Kobayashi:
A Temporal Logic for Higher-Order Functional Programs. SAS 2019: 437-458 - [i9]Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada:
A Type-Based HFL Model Checking Algorithm. CoRR abs/1908.10416 (2019) - 2018
- [j29]Magnús M. Halldórsson, Naoki Kobayashi, Bettina Speckmann:
Special issue for the 42nd International Colloquium on Automata, Languages and Programming, ICALP 2015, Kyoto, Japan. Inf. Comput. 261: 159 (2018) - [c105]Adrien Champion, Naoki Kobayashi, Ryosuke Sato:
HoIce: An ICE-Based Non-linear Horn Clause Solver. APLAS 2018: 146-156 - [c104]Shingo Eguchi, Naoki Kobayashi, Takeshi Tsukada:
Automated Synthesis of Functional Programs with Auxiliary Functions. APLAS 2018: 223-241 - [c103]Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe:
Higher-Order Program Verification via HFL Model Checking. ESOP 2018: 711-738 - [c102]Kazuyuki Asada, Naoki Kobayashi:
Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered. FSTTCS 2018: 14:1-14:15 - [c101]Adrien Champion, Tomoya Chiba, Naoki Kobayashi, Ryosuke Sato:
ICE-Based Refinement Type Discovery for Higher-Order Functional Programs. TACAS (1) 2018: 365-384 - [i8]Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada:
Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence. CoRR abs/1801.03886 (2018) - [i7]Naoki Kobayashi, Ugo Dal Lago, Charles Grellois:
On the Termination Problem for Probabilistic Higher-Order Recursive Programs. CoRR abs/1811.02133 (2018) - 2017
- [j28]Naoki Kobayashi, Cosimo Laneve:
Deadlock analysis of unbounded process networks. Inf. Comput. 252: 48-70 (2017) - [j27]Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi:
Verifying relational properties of functional programs by first-order refinement. Sci. Comput. Program. 137: 2-62 (2017) - [c100]Ryosuke Sato, Naoki Kobayashi:
Modular Verification of Higher-Order Functional Programs. ESOP 2017: 831-854 - [c99]Ryoma Sin'ya, Kazuyuki Asada, Naoki Kobayashi, Takeshi Tsukada:
Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence. FoSSaCS 2017: 53-68 - [c98]Kazuyuki Asada, Naoki Kobayashi:
Pumping Lemma for Higher-order Languages. ICALP 2017: 97:1-97:14 - [c97]Takashi Suwa, Takeshi Tsukada, Naoki Kobayashi, Atsushi Igarashi:
Verification of code generators via higher-order model checking. PEPM 2017: 59-70 - [c96]Naoki Kobayashi, Étienne Lozes, Florian Bruse:
On the relationship between higher-order recursion schemes and higher-order fixpoint logic. POPL 2017: 246-259 - [c95]Ryota Suzuki, Koichi Fujima, Naoki Kobayashi, Takeshi Tsukada:
Streett Automata Model Checking of Higher-Order Recursion Schemes. FSCD 2017: 32:1-32:18 - [e7]Naoki Kobayashi:
Proceedings Eighth Workshop on Intersection Types and Related Systems, ITRS 2016, Porto, Portugal, 26th June 2016. EPTCS 242, 2017 [contents] - [i6]Kazuyuki Asada, Naoki Kobayashi:
Pumping Lemma for Higher-order Languages. CoRR abs/1705.10699 (2017) - [i5]Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe:
Higher-Order Program Verification via HFL Model Checking. CoRR abs/1710.08614 (2017) - 2016
- [c94]Taku Terao, Takeshi Tsukada, Naoki Kobayashi:
Higher-Order Model Checking in Direct Style. APLAS 2016: 295-313 - [c93]Kazuhide Yasukata, Takeshi Tsukada, Naoki Kobayashi:
Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation. APLAS 2016: 335-353 - [c92]Xin Li, Naoki Kobayashi:
Equivalence-Based Abstraction Refinement for \mu HORS Model Checking. ATVA 2016: 304-320 - [c91]Kazuyuki Asada, Naoki Kobayashi:
On Word and Frontier Languages of Unsafe Higher-Order Grammars. ICALP 2016: 111:1-111:13 - [c90]Kotaro Takeda, Naoki Kobayashi, Kazuya Yaguchi, Ayumi Shinohara:
Compact bit encoding schemes for simply-typed lambda-terms. ICFP 2016: 146-157 - [c89]Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, Naoki Kobayashi:
Automatically disproving fair termination of higher-order functional programs. ICFP 2016: 243-255 - [c88]Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno:
Temporal verification of higher-order functional programs. POPL 2016: 57-68 - [i4]Kazuyuki Asada, Naoki Kobayashi:
On Word and Frontier Languages of Unsafe Higher-Order Grammars. CoRR abs/1604.01595 (2016) - [i3]Naoki Kobayashi, Luke Ong, Igor Walukiewicz:
Higher-Order Model Checking (NII Shonan Meeting 2016-4). NII Shonan Meet. Rep. 2016 (2016) - 2015
- [j26]Ryosuke Sato, Kazuyuki Asada, Naoki Kobayashi:
Refinement Type Checking via Assertion Checking. J. Inf. Process. 23(6): 827-834 (2015) - [j25]Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi:
Verification of tree-processing programs via higher-order mode checking. Math. Struct. Comput. Sci. 25(4): 841-866 (2015) - [c87]Yuma Matsumoto, Naoki Kobayashi, Hiroshi Unno:
Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs. APLAS 2015: 295-312 - [c86]Sadaaki Kawata, Kazuyuki Asada, Naoki Kobayashi:
Decision Algorithms for Checking Definability of Order-2 Finitary PCF. APLAS 2015: 313-331 - [c85]Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi:
Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs. CAV (2) 2015: 287-303 - [c84]Naoki Kobayashi, Xin Li:
Automata-Based Abstraction Refinement for µHORS Model Checking. LICS 2015: 713-724 - [c83]Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi:
Verifying Relational Properties of Functional Programs by First-Order Refinement. PEPM 2015: 61-72 - [e6]Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, Bettina Speckmann:
Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part I. Lecture Notes in Computer Science 9134, Springer 2015, ISBN 978-3-662-47671-0 [contents] - [e5]Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, Bettina Speckmann:
Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II. Lecture Notes in Computer Science 9135, Springer 2015, ISBN 978-3-662-47665-9 [contents] - 2014
- [c82]Taku Terao, Naoki Kobayashi:
A ZDD-Based Efficient Higher-Order Model Checking Algorithm. APLAS 2014: 354-371 - [c81]Naoki Kobayashi:
From Linear Types to Behavioural Types and Model Checking. Concurrent Objects and Beyond 2014: 128-143 - [c80]Elena Giachino, Naoki Kobayashi, Cosimo Laneve:
Deadlock Analysis of Unbounded Process Networks. CONCUR 2014: 63-77 - [c79]Kazuhide Yasukata, Naoki Kobayashi, Kazutaka Matsuda:
Pairwise Reachability Analysis for Higher Order Concurrent Programs by Higher-Order Model Checking. CONCUR 2014: 312-326 - [c78]Kazuya Yaguchi, Naoki Kobayashi, Ayumi Shinohara:
Efficient Algorithm and Coding for Higher-Order Compression. DCC 2014: 434 - [c77]Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi:
Automatic Termination Verification for Higher-Order Functional Programs. ESOP 2014: 392-411 - [c76]Naoki Kobayashi, Kazuhiro Inaba, Takeshi Tsukada:
Unsafe Order-2 Tree Languages Are Context-Sensitive. FoSSaCS 2014: 149-163 - [c75]Takeshi Tsukada, Naoki Kobayashi:
Complexity of Model-Checking Call-by-Value Programs. FoSSaCS 2014: 180-194 - [e4]Gul A. Agha, Atsushi Igarashi, Naoki Kobayashi, Hidehiko Masuhara, Satoshi Matsuoka, Etsuya Shibayama, Kenjiro Taura:
Concurrent Objects and Beyond - Papers dedicated to Akinori Yonezawa on the Occasion of His 65th Birthday. Lecture Notes in Computer Science 8665, Springer 2014, ISBN 978-3-662-44470-2 [contents] - 2013
- [j24]Naoki Kobayashi:
Model Checking Higher-Order Programs. J. ACM 60(3): 20:1-20:62 (2013) - [c74]Koichi Fujima, Sohei Ito, Naoki Kobayashi:
Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes. APLAS 2013: 17-32 - [c73]Christopher H. Broadbent, Naoki Kobayashi:
Saturation-Based Model Checking of Higher-Order Recursion Schemes. CSL 2013: 129-148 - [c72]Naoki Kobayashi, Atsushi Igarashi:
Model-Checking Higher-Order Programs with Recursive Types. ESOP 2013: 431-450 - [c71]Naoki Kobayashi:
Pumping by Typing. LICS 2013: 398-407 - [c70]Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi:
Towards a scalable software model checker for higher-order programs. PEPM 2013: 53-62 - [c69]Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi:
Automating relatively complete verification of higher-order functional programs. POPL 2013: 75-86 - 2012
- [j23]Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara, Kazuya Yaguchi:
Functional programs as compressed data. High. Order Symb. Comput. 25(1): 39-84 (2012) - [c68]Naoki Kobayashi:
Program Certification by Higher-Order Model Checking. CPP 2012: 9-10 - [c67]Yoshihiro Tobita, Takeshi Tsukada, Naoki Kobayashi:
Exact Flow Analysis by Higher-Order Model Checking. FLOPS 2012: 275-289 - [c66]Takeshi Tsukada, Naoki Kobayashi:
An Intersection Type System for Deterministic Pushdown Automata. IFIP TCS 2012: 357-371 - [c65]Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara:
Functional programs as compressed data. PEPM 2012: 121-130 - 2011
- [j22]Naoki Kobayashi, C.-H. Luke Ong:
Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus. Log. Methods Comput. Sci. 7(4) (2011) - [j21]Ryosuke Sato, Kohei Suenaga, Naoki Kobayashi:
Ordered Types for Stream Processing of Tree-Structured Data. Inf. Media Technol. 6(2): 385-398 (2011) - [j20]Ryosuke Sato, Kohei Suenaga, Naoki Kobayashi:
Ordered Types for Stream Processing of Tree-Structured Data. J. Inf. Process. 19: 74-87 (2011) - [j19]Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii:
Environmental bisimulations for higher-order languages. ACM Trans. Program. Lang. Syst. 33(1): 5:1-5:69 (2011) - [c64]Morten Dahl, Naoki Kobayashi, Yunde Sun, Hans Hüttel:
Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols. ATVA 2011: 75-89 - [c63]Naoki Kobayashi:
A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes. FoSSaCS 2011: 260-274 - [c62]Naoki Kobayashi:
Higher-Order Model Checking: From Theory to Practice. LICS 2011: 219-224 - [c61]Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno:
Predicate abstraction and CEGAR for higher-order model checking. PLDI 2011: 222-233 - [i2]Naoki Kobayashi, Luke Ong, David Van Horn:
Automated Techniques for Higher-Order Program Verification (NII Shonan Meeting 2011-5). NII Shonan Meet. Rep. 2011 (2011) - 2010
- [j18]Naoki Kobayashi, Davide Sangiorgi:
A hybrid type system for lock-freedom of mobile processes. ACM Trans. Program. Lang. Syst. 32(5): 16:1-16:49 (2010) - [c60]Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi:
Verification of Tree-Processing Programs via Higher-Order Model Checking. APLAS 2010: 312-327 - [c59]Takeshi Tsukada, Naoki Kobayashi:
Untyped Recursion Schemes and Infinite Intersection Types. FoSSaCS 2010: 343-357 - [c58]Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno:
Higher-order multi-parameter tree transducers and recursion schemes for program verification. POPL 2010: 495-508 - [e3]Matthias Blume, Naoki Kobayashi, Germán Vidal:
Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings. Lecture Notes in Computer Science 6009, Springer 2010, ISBN 978-3-642-12250-7 [contents]
2000 – 2009
- 2009
- [j17]Hans Hüttel, Naoki Kobayashi, Takashi Suto:
Undecidable equivalences for basic parallel processes. Inf. Comput. 207(7): 812-829 (2009) - [c57]Naoki Kobayashi:
Types and Recursion Schemes for Higher-Order Program Verification. APLAS 2009: 2-3 - [c56]Kohei Suenaga, Naoki Kobayashi:
Fractional Ownerships for Safe Memory Deallocation. APLAS 2009: 128-143 - [c55]Naoki Kobayashi:
Higher-Order Program Verification and Language-Based Security. ASIAN 2009: 17-23 - [c54]Daisuke Kikuchi, Naoki Kobayashi:
Type-Based Automated Verification of Authenticity in Cryptographic Protocols. ESOP 2009: 222-236 - [c53]Naoki Kobayashi, C.-H. Luke Ong:
Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus. ICALP (2) 2009: 223-234 - [c52]Naoki Kobayashi, C.-H. Luke Ong:
A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes. LICS 2009: 179-188 - [c51]Naoki Kobayashi:
Types and higher-order recursion schemes for verification of higher-order programs. POPL 2009: 416-428 - [c50]Naoki Kobayashi:
Model-checking higher-order functions. PPDP 2009: 25-36 - [c49]Hiroshi Unno, Naoki Kobayashi:
Dependent type inference with interpolants. PPDP 2009: 277-288 - 2008
- [j16]Koichi Kodama, Kohei Suenaga, Naoki Kobayashi:
Translation of tree-processing programs into stream-processing programs based on ordered linear type. J. Funct. Program. 18(3): 333-371 (2008) - [j15]Futoshi Iwama, Naoki Kobayashi:
A New Type System for JVM Lock Primitives. New Gener. Comput. 26(2): 125-170 (2008) - [c48]Naoki Kobayashi, Davide Sangiorgi:
A Hybrid Type System for Lock-Freedom of Mobile Processes. CAV 2008: 80-93 - [c47]Yûta Kaneko, Naoki Kobayashi:
Linear Declassification. ESOP 2008: 224-238 - [c46]Naoki Kobayashi:
Substructural Type Systems for Program Analysis. FLOPS 2008: 14 - [c45]Hiroshi Unno, Naoki Kobayashi:
On-Demand Refinement of Dependent Types. FLOPS 2008: 81-96 - [c44]Naoki Kobayashi, Hitoshi Ohsaki:
Tree Automata for Non-linear Arithmetic. RTA 2008: 291-305 - 2007
- [c43]Daisuke Kikuchi, Naoki Kobayashi:
Type-Based Verification of Correspondence Assertions for Communication Protocols. APLAS 2007: 191-205 - [c42]Kohei Suenaga, Naoki Kobayashi:
Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts. ESOP 2007: 490-504 - [c41]Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii:
Logical Bisimulations and Functional Languages. FSEN 2007: 364-379 - [c40]Naoki Kobayashi, Takashi Suto:
Undecidability of 2-Label BPP Equivalences and Behavioral Type Systems for the pi -Calculus. ICALP 2007: 740-751 - [c39]Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii:
Environmental Bisimulations for Higher-Order Languages. LICS 2007: 293-302 - [c38]Romain Demangeon, Daniel Hirschkoff, Naoki Kobayashi, Davide Sangiorgi:
On the Complexity of Termination Inference for Processes. TGC 2007: 140-155 - 2006
- [j14]Naoki Kobayashi, Kohei Suenaga, Lucian Wischik:
Resource Usage Analysis for the p-Calculus. Log. Methods Comput. Sci. 2(3) (2006) - [c37]Naoki Kobayashi:
A New Type System for Deadlock-Free Processes. CONCUR 2006: 233-247 - [c36]Futoshi Iwama, Atsushi Igarashi, Naoki Kobayashi:
Resource usage analysis for a functional language with exceptions. PEPM 2006: 38-47 - [c35]Hiroshi Unno, Naoki Kobayashi, Akinori Yonezawa:
Combining type-based analysis and model checking for finding counterexamples against non-interference. PLAS 2006: 17-26 - [c34]Naoki Kobayashi, Kohei Suenaga, Lucian Wischik:
Resource Usage Analysis for the pi-Calculus. VMCAI 2006: 298-312 - [e2]Naoki Kobayashi:
Programming Languages and Systems, 4th Asian Symposium, APLAS 2006, Sydney, Australia, November 8-10, 2006, Proceedings. Lecture Notes in Computer Science 4279, Springer 2006, ISBN 3-540-48937-1 [contents] - [i1]Naoki Kobayashi, Kohei Suenaga, Lucian Wischik:
Resource Usage Analysis for the Pi-Calculus. CoRR abs/cs/0608035 (2006) - 2005
- [j13]Naoki Kobayashi:
Type-based information flow analysis for the pi-calculus. Acta Informatica 42(4-5): 291-347 (2005) - [j12]Atsushi Igarashi, Naoki Kobayashi:
Resource usage analysis. ACM Trans. Program. Lang. Syst. 27(2): 264-313 (2005) - [c33]Kohei Suenaga, Naoki Kobayashi, Akinori Yonezawa:
Extension of Type-Based Approach to Generation of Stream-Processing Programs by Automatic Insertion of Buffering Primitives. LOPSTR 2005: 98-114 - 2004
- [j11]Atsushi Igarashi, Naoki Kobayashi:
A generic type system for the Pi-calculus. Theor. Comput. Sci. 311(1-3): 121-163 (2004) - [c32]Koichi Kodama, Kohei Suenaga, Naoki Kobayashi:
Translation of Tree-Processing Programs into Stream-Processing Programs Based on Ordered Linear Type. APLAS 2004: 41-56 - [c31]Akihito Nagata, Naoki Kobayashi, Akinori Yonezawa:
Region-Based Memory Management for a Dynamically-Typed Language. APLAS 2004: 229-245 - [c30]Reynald Affeldt, Naoki Kobayashi:
A Coq Library for Verification of Concurrent Programs. LFM@IJCAR 2004: 17-32 - [c29]Reynald Affeldt, Naoki Kobayashi:
Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes. EXPRESS 2004: 151-168 - 2003
- [j10]Naoki Kobayashi, Benjamin C. Pierce:
Information and Computation special issue from TACS 2001. Inf. Comput. 186(2): 163-164 (2003) - [c28]Naoki Kobayashi:
Useless Code Elimination and Programm Slicing for the Pi-Calculus. APLAS 2003: 55-72 - [c27]Naoki Kobayashi:
Time regions and effects for resource usage analysis. TLDI 2003: 50-61 - 2002
- [j9]Naoki Kobayashi:
A Type System for Lock-Free Processes. Inf. Comput. 177(2): 122-159 (2002) - [c26]Naoki Kobayashi, Keita Shirane:
Type-Based Information Analysis for Low-Level Languages. APLAS 2002: 302-316 - [c25]Etsuya Shibayama, Shigeki Hagihara, Naoki Kobayashi, Shin-ya Nishizaki, Kenjiro Taura, Takuo Watanabe:
AnZenMail: A Secure and Certified E-mail System. ISSS 2002: 201-216 - [c24]Reynald Affeldt, Naoki Kobayashi:
Formalization and Verification of a Mail Server in Coq. ISSS 2002: 217-233 - [c23]Futoshi Iwama, Naoki Kobayashi:
A new type system for JVM lock primitives. ASIA-PEPM 2002: 71-82 - [c22]Atsushi Igarashi, Naoki Kobayashi:
Resource usage analysis. POPL 2002: 331-342 - [c21]Naoki Kobayashi:
Type Systems for Concurrent Programs. 10th Anniversary Colloquium of UNU/IIST 2002: 439-453 - 2001
- [j8]Eijiro Sumii, Naoki Kobayashi:
A Hybrid Approach to Online and Offline Partial Evaluation. High. Order Symb. Comput. 14(2-3): 101-142 (2001) - [j7]Naoki Kobayashi:
Type-Based Useless-Variable Elimination. High. Order Symb. Comput. 14(2-3): 221-260 (2001) - [c20]Atsushi Igarashi, Naoki Kobayashi:
Resource Usage Analysis. APLAS 2001: 147-158 - [c19]Atsushi Igarashi, Naoki Kobayashi:
A generic type system for the Pi-calculus. POPL 2001: 128-141 - [e1]Naoki Kobayashi, Benjamin C. Pierce:
Theoretical Aspects of Computer Software, 4th International Symposium, TACS 2001, Sendai, Japan, October 29-31, 2001, Proceedings. Lecture Notes in Computer Science 2215, Springer 2001, ISBN 3-540-42736-8 [contents] - 2000
- [j6]Atsushi Igarashi, Naoki Kobayashi:
Type Reconstruction for Linear -Calculus with I/O Subtyping. Inf. Comput. 161(1): 1-44 (2000) - [c18]Naoki Kobayashi, Shin Saito, Eijiro Sumii:
An Implicitly-Typed Deadlock-Free Process Calculus. CONCUR 2000: 489-503 - [c17]Naoki Kobayashi:
Type Systems for Concurrent Processes: From Deadlock-Freedom to Livelock-Freedom, Time-Boundedness. IFIP TCS 2000: 365-389 - [c16]Eijiro Sumii, Naoki Kobayashi:
Online-and-Offline Partial Evaluation: A Mixed Approach (Extended Abstract). PEPM 2000: 12-21 - [c15]Naoki Kobayashi:
Type-Based Useless Variable Elimination. PEPM 2000: 84-93
1990 – 1999
- 1999
- [j5]Naoki Kobayashi, Toshihiro Shimizu, Akinori Yonezawa:
Distributed Concurrent Linear Logic Programming. Theor. Comput. Sci. 227(1-2): 185-220 (1999) - [j4]Naoki Kobayashi, Benjamin C. Pierce, David N. Turner:
Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst. 21(5): 914-947 (1999) - [c14]Naoki Kobayashi, Akinori Yonezawa:
Distributed and concurrent objects based on linear logic (Invited Talk). FMOODS 1999 - [c13]Naoki Kobayashi:
Quasi-Linear Types. POPL 1999: 29-42 - 1998
- [j3]Naoki Kobayashi:
A Partially Deadlock-Free Typed Process Calculus. ACM Trans. Program. Lang. Syst. 20(2): 436-482 (1998) - [c12]Naoki Kobayashi:
Type-Based Analysis of Concurrent Programs. Types in Compilation 1998: 272 - [c11]Eijiro Sumii, Naoki Kobayashi:
A Generalized Deadlock-Free Process Calculus. HLCL 1998: 225-247 - 1997
- [c10]Naoki Kobayashi:
A Partially Deadlock-Free Typed Process Calculus. LICS 1997: 128-139 - [c9]Atsushi Igarashi, Naoki Kobayashi:
Type-Based Analysis of Communication for Concurrent Programming Languages. SAS 1997: 187-201 - 1996
- [c8]Haruo Hosoya, Naoki Kobayashi, Akinori Yonezawa:
Partial Evaluation Scheme for Concurrent Languages and Its Correctness. Euro-Par, Vol. I 1996: 625-632 - [c7]Naoki Kobayashi, Benjamin C. Pierce, David N. Turner:
Linearity and the Pi-Calculus. POPL 1996: 358-371 - 1995
- [j2]Naoki Kobayashi, Akinori Yonezawa:
Asynchronous Communication Model Based on Linear Logic. Formal Aspects Comput. 7(2): 113-149 (1995) - [j1]Naoki Kobayashi, Akinori Yonezawa:
Towards Foundations of Concurrent Object-Oriented Programming-Types and Language Design. Theory Pract. Object Syst. 1(4): 243-268 (1995) - [c6]Naoki Kobayashi, Motoki Nakade, Akinori Yonezawa:
Static Analysis of Communication for Asynchronous Concurrent Programming Languages. SAS 1995: 225-242 - 1994
- [c5]Naoki Kobayashi, Akinori Yonezawa:
Type-Theoretic Foundations for Concurrent Object-Oriented Programming. OOPSLA 1994: 31-45 - [c4]Kazuhiro Konno, Masaaki Nagatsuka, Naoki Kobayashi, Satoshi Matsuoka, Akinori Yonezawa:
PARCS: An MPP-Oriented CLP Language. PASCO 1994: 254-263 - [c3]Naoki Kobayashi, Akinori Yonezawa:
Higher-Order Concurrent Linear Logic Programming. Theory and Practice of Parallel Programming 1994: 137-166 - 1993
- [c2]Naoki Kobayashi, Akinori Yonezawa:
ACL - A Concurrent Linear Logic Programming Paradigm. ILPS 1993: 279-294 - 1992
- [c1]Naoki Kobayashi, Akinori Yonezawa:
Asynchronous Communication Model Based on Linear Logic. Parallel Symbolic Computing 1992: 331-336
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-08 02:23 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
