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)- [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]