Naoki Kobayashi

220 papers A* 22A 13B 55C 13Misc 5Journal 67Unranked 38

Year	Rank	Type	Title / Venue / Authors
2026	—	`conf`	Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators. ESOP (2) Izumi Tanaka, Ken Sakayori, Shinya Takamaeda-Yamazaki, Naoki Kobayashi
2026	J	`jnl`	Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators. CoRR Izumi Tanaka, Ken Sakayori, Shinya Takamaeda-Yamazaki, Naoki Kobayashi
2025	B	`conf`	Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types. SAS Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato
2025	J	`jnl`	Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types. CoRR Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato
2025	J	`jnl`	On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus. Proc. ACM Program. Lang. Naoki Kobayashi
2025	—	`conf`	On the Relationship between Dijkstra Monads and Higher-Order Fixpoint Logic. ESOP (2) Risa Yamada, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato
2025	J	`jnl`	Solvable Tuple Patterns and Their Applications to Program Verification. CoRR Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara, Ryo Yoshinaka
2025	J	`jnl`	Towards neural-network-guided program synthesis and verification. Formal Methods Syst. Des. Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno
2024	J	`jnl`	Asynchronous unfold/fold transformation for fixpoint logic. Sci. Comput. Program. Mahmudul Faisal Al Ameen, Naoki Kobayashi, Ryosuke Sato
2024	—	`conf`	Borrowable Fractional Ownership Types for Verification. VMCAI (2) Takashi Nakayama, Yusuke Matsushita, Ken Sakayori, Ryosuke Sato, Naoki Kobayashi
2024	J	`jnl`	FoSSaCS 2024: Report of the Program Chairs. ACM SIGLOG News Naoki Kobayashi, James Worrell
2024	—	`ed.`	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 FoSSaCS (1) Naoki Kobayashi, James Worrell
2024	—	`ed.`	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 FoSSaCS (2) Naoki Kobayashi, James Worrell
2024	B	`conf`	Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem. APLAS Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato
2024	C	`conf`	Ownership Types for Verification of Programs with Pointer Arithmetic. PEPM Izumi Tanaka, Ken Sakayori, Naoki Kobayashi
2024	C	`conf`	Productivity Verification for Functional Programs by Reduction to Termination Verification. PEPM Ren Fukaishi, Naoki Kobayashi, Ryosuke Sato
2023	B	`conf`	Argument Reduction of Constrained Horn Clauses Using Equality Constraints. APLAS Ryo Ikeda, Ryosuke Sato, Naoki Kobayashi
2023	J	`jnl`	Borrowable Fractional Ownership Types for Verification. CoRR Takashi Nakayama, Yusuke Matsushita, Ken Sakayori, Ryosuke Sato, Naoki Kobayashi
2023	A	`conf`	Gradual Tensor Shape Checking. ESOP Momoko Hattori, Naoki Kobayashi, Ryosuke Sato
2023	J	`jnl`	HFL(Z) Validity Checking for Automated Program Verification. Proc. ACM Program. Lang. Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, Takeshi Tsukada
2023	J	`jnl`	Higher-Order Property-Directed Reachability. Proc. ACM Program. Lang. Hiroyuki Katsura, Naoki Kobayashi, Ryosuke Sato
2023	—	`conf`	Neural Network-Guided Synthesis of Recursive List Functions. TACAS (1) Naoki Kobayashi, Minchao Wu
2023	J	`jnl`	Ownership Types for Verification of Programs with Pointer Arithmetic. CoRR Izumi Tanaka, Ken Sakayori, Naoki Kobayashi
2022	Misc	`conf`	Asynchronous Unfold/Fold Transformation for Fixpoint Logic. FLOPS Mahmudul Faisal Al Ameen, Naoki Kobayashi, Ryosuke Sato
2022	J	`jnl`	Automatic HFL(Z) Validity Checking for Program Verification. CoRR Kento Tanahashi, Naoki Kobayashi, Ryosuke Sato
2022	J	`jnl`	Gradual Tensor Shape Checking. CoRR Momoko Hattori, Naoki Kobayashi, Ryosuke Sato
2022	—	`conf`	On Higher-Order Reachability Games Vs May Reachability. RP Kazuyuki Asada, Hiroyuki Katsura, Naoki Kobayashi
2022	J	`jnl`	On Higher-Order Reachability Games vs May Reachability. CoRR Kazuyuki Asada, Hiroyuki Katsura, Naoki Kobayashi
2022	B	`conf`	Parameterized Recursive Refinement Types for Automated Program Verification. SAS Ryoya Mukai, Naoki Kobayashi, Ryosuke Sato
2021	B	`ed.`	6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, Buenos Aires, Argentina (Virtual Conference), July 17-24, 2021 FSCD Naoki Kobayashi
2021	B	`conf`	A Cyclic Proof System for HFL_ℕ. CSL Mayuko Kori, Takeshi Tsukada, Naoki Kobayashi
2021	J	`jnl`	A Probabilistic Higher-order Fixpoint Logic. Log. Methods Comput. Sci. Yo Mitani, Naoki Kobayashi, Takeshi Tsukada
2021	—	`conf`	An Overview of the HFL Model Checking Project. HCVS@ETAPS Naoki Kobayashi
2021	—	`conf`	Counterexample generation for program verification based on ownership refinement types. PEPM@POPL Hideto Ueno, John Toman, Naoki Kobayashi, Takeshi Tsukada
2021	—	`conf`	Inside-Outside Algorithm for Macro Grammars. ICGI Ryuta Kambe, Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara, Ryo Yoshinaka
2021	J	`jnl`	RustHorn: CHC-based Verification for Rust Programs. ACM Trans. Program. Lang. Syst. Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi
2021	B	`conf`	Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes. CONCUR Patrick Baillot, Alexis Ghyselen, Naoki Kobayashi
2021	J	`jnl`	Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes. CoRR Patrick Baillot, Alexis Ghyselen, Naoki Kobayashi
2021	B	`conf`	Symbolic Automatic Relations and Their Applications to SMT and CHC Solving. SAS Takumi Shimoda, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato
2021	J	`jnl`	Symbolic Automatic Relations and Their Applications to SMT and CHC Solving. CoRR Takumi Shimoda, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato
2021	B	`conf`	Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination. APLAS Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada
2021	J	`jnl`	Termination Analysis for the π-Calculus by Reduction to Sequential Program Termination. CoRR Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada
2021	B	`conf`	Toward Neural-Network-Guided Program Synthesis and Verification. SAS Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno
2021	J	`jnl`	Toward Neural-Network-Guided Program Synthesis and Verification. CoRR Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno
2020	J	`jnl`	A Cyclic Proof System for HFLN. CoRR Mayuko Kori, Takeshi Tsukada, Naoki Kobayashi
2020	B	`conf`	A New Refinement Type System for Automated $\nu \text {HFL}_\mathbb {Z}$ Validity Checking. APLAS Hiroyuki Katsura, Naoki Iwayama, Naoki Kobayashi, Takeshi Tsukada
2020	B	`conf`	A Probabilistic Higher-Order Fixpoint Logic. FSCD Yo Mitani, Naoki Kobayashi, Takeshi Tsukada
2020	J	`jnl`	A Probabilistic Higher-order Fixpoint Logic. CoRR Yo Mitani, Naoki Kobayashi, Takeshi Tsukada
2020	A	`conf`	ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs. ESOP John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, Naoki Kobayashi
2020	J	`jnl`	ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs. CoRR John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, Naoki Kobayashi
2020	—	`conf`	Fold/Unfold Transformations for Fixpoint Logic. TACAS (2) Naoki Kobayashi, Grigory Fedyukovich, Aarti Gupta
2020	B	`conf`	Grammar Compression with Probabilistic Context-Free Grammar. DCC Hiroaki Naganuma, Diptarama Hendrian, Ryo Yoshinaka, Ayumi Shinohara, Naoki Kobayashi
2020	J	`jnl`	Grammar compression with probabilistic context-free grammar. CoRR Hiroaki Naganuma, Diptarama Hendrian, Ryo Yoshinaka, Ayumi Shinohara, Naoki Kobayashi
2020	J	`jnl`	ICE-Based Refinement Type Discovery for Higher-Order Functional Programs. J. Autom. Reason. Adrien Champion, Tomoya Chiba, Naoki Kobayashi, Ryosuke Sato
2020	A*	`ed.`	LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020. LICS Holger Hermanns, Lijun Zhang, Naoki Kobayashi, Dale Miller
2020	B	`conf`	On Average-Case Hardness of Higher-Order Model Checking. FSCD Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada
2020	J	`jnl`	On the Termination Problem for Probabilistic Higher-Order Recursive Programs. Log. Methods Comput. Sci. Naoki Kobayashi, Ugo Dal Lago, Charles Grellois
2020	B	`conf`	Predicate Abstraction and CEGAR for $\nu \mathrm {HFL}_\mathbb {Z}$ Validity Checking. SAS Naoki Iwayama, Naoki Kobayashi, Ryota Suzuki, Takeshi Tsukada
2020	A	`conf`	RustHorn: CHC-Based Verification for Rust Programs. ESOP Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi
2020	J	`jnl`	RustHorn: CHC-based Verification for Rust Programs (full version). CoRR Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi
2020	B	`conf`	Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars. FSCD Kazuyuki Asada, Naoki Kobayashi
2019	C	`conf`	10 Years of the Higher-Order Model Checking Project (Extended Abstract). PPDP Naoki Kobayashi
2019	B	`conf`	A Temporal Logic for Higher-Order Functional Programs. SAS Yuya Okuyama, Takeshi Tsukada, Naoki Kobayashi
2019	B	`conf`	A Type-Based HFL Model Checking Algorithm. APLAS Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada
2019	J	`jnl`	A Type-Based HFL Model Checking Algorithm. CoRR Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada
2019	J	`jnl`	Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence. Log. Methods Comput. Sci. Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada
2019	—	`conf`	Combining higher-order model checking with refinement type inference. PEPM@POPL Ryosuke Sato, Naoki Iwayama, Naoki Kobayashi
2019	J	`jnl`	Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable. Theor. Comput. Sci. Naoki Kobayashi
2019	A*	`conf`	On the Termination Problem for Probabilistic Higher-Order Recursive Programs. LICS Naoki Kobayashi, Ugo Dal Lago, Charles Grellois
2019	—	`conf`	Reduction from branching-time property verification of higher-order programs to HFL validity checking. PEPM@POPL Keiichi Watanabe, Takeshi Tsukada, Hiroki Oshikawa, Naoki Kobayashi
2019	B	`conf`	Temporal Verification of Programs via First-Order Fixpoint Logic. SAS Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, Hiroshi Unno
2018	J	`jnl`	Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence. CoRR Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada
2018	B	`conf`	Automated Synthesis of Functional Programs with Auxiliary Functions. APLAS Shingo Eguchi, Naoki Kobayashi, Takeshi Tsukada
2018	A	`conf`	Higher-Order Program Verification via HFL Model Checking. ESOP Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe
2018	B	`conf`	HoIce: An ICE-Based Non-linear Horn Clause Solver. APLAS Adrien Champion, Naoki Kobayashi, Ryosuke Sato
2018	—	`conf`	ICE-Based Refinement Type Discovery for Higher-Order Functional Programs. TACAS (1) Adrien Champion, Tomoya Chiba, Naoki Kobayashi, Ryosuke Sato
2018	—	`conf`	Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered. FSTTCS Kazuyuki Asada, Naoki Kobayashi
2018	J	`jnl`	On the Termination Problem for Probabilistic Higher-Order Recursive Programs. CoRR Naoki Kobayashi, Ugo Dal Lago, Charles Grellois
2018	J	`jnl`	Special issue for the 42nd International Colloquium on Automata, Languages and Programming, ICALP 2015, Kyoto, Japan. Inf. Comput. Magnús M. Halldórsson, Naoki Kobayashi, Bettina Speckmann
2017	B	`conf`	Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence. FoSSaCS Ryoma Sin'ya, Kazuyuki Asada, Naoki Kobayashi, Takeshi Tsukada
2017	J	`jnl`	Deadlock analysis of unbounded process networks. Inf. Comput. Naoki Kobayashi, Cosimo Laneve
2017	J	`jnl`	Higher-Order Program Verification via HFL Model Checking. CoRR Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe
2017	A	`conf`	Modular Verification of Higher-Order Functional Programs. ESOP Ryosuke Sato, Naoki Kobayashi
2017	A*	`conf`	On the relationship between higher-order recursion schemes and higher-order fixpoint logic. POPL Naoki Kobayashi, Étienne Lozes, Florian Bruse
2017	—	`ed.`	Proceedings Eighth Workshop on Intersection Types and Related Systems, ITRS 2016, Porto, Portugal, 26th June 2016. ITRS Naoki Kobayashi
2017	A*	`conf`	Pumping Lemma for Higher-order Languages. ICALP Kazuyuki Asada, Naoki Kobayashi
2017	J	`jnl`	Pumping Lemma for Higher-order Languages. CoRR Kazuyuki Asada, Naoki Kobayashi
2017	B	`conf`	Streett Automata Model Checking of Higher-Order Recursion Schemes. FSCD Ryota Suzuki, Koichi Fujima, Naoki Kobayashi, Takeshi Tsukada
2017	C	`conf`	Verification of code generators via higher-order model checking. PEPM Takashi Suwa, Takeshi Tsukada, Naoki Kobayashi, Atsushi Igarashi
2017	J	`jnl`	Verifying relational properties of functional programs by first-order refinement. Sci. Comput. Program. Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi
2016	A	`conf`	Automatically disproving fair termination of higher-order functional programs. ICFP Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, Naoki Kobayashi
2016	A	`conf`	Compact bit encoding schemes for simply-typed lambda-terms. ICFP Kotaro Takeda, Naoki Kobayashi, Kazuya Yaguchi, Ayumi Shinohara
2016	B	`conf`	Equivalence-Based Abstraction Refinement for \mu HORS Model Checking. ATVA Xin Li, Naoki Kobayashi
2016	J	`jnl`	Higher-Order Model Checking (NII Shonan Meeting 2016-4). NII Shonan Meet. Rep. Naoki Kobayashi, Luke Ong, Igor Walukiewicz
2016	B	`conf`	Higher-Order Model Checking in Direct Style. APLAS Taku Terao, Takeshi Tsukada, Naoki Kobayashi
2016	A*	`conf`	On Word and Frontier Languages of Unsafe Higher-Order Grammars. ICALP Kazuyuki Asada, Naoki Kobayashi
2016	J	`jnl`	On Word and Frontier Languages of Unsafe Higher-Order Grammars. CoRR Kazuyuki Asada, Naoki Kobayashi
2016	A*	`conf`	Temporal verification of higher-order functional programs. POPL Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno
2016	B	`conf`	Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation. APLAS Kazuhide Yasukata, Takeshi Tsukada, Naoki Kobayashi
2015	—	`ed.`	Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part I ICALP (1) Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, Bettina Speckmann
2015	—	`ed.`	Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II ICALP (2) Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, Bettina Speckmann
2015	A*	`conf`	Automata-Based Abstraction Refinement for µHORS Model Checking. LICS Naoki Kobayashi, Xin Li
2015	B	`conf`	Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs. APLAS Yuma Matsumoto, Naoki Kobayashi, Hiroshi Unno
2015	B	`conf`	Decision Algorithms for Checking Definability of Order-2 Finitary PCF. APLAS Sadaaki Kawata, Kazuyuki Asada, Naoki Kobayashi
2015	—	`conf`	Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs. CAV (2) Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi
2015	J	`jnl`	Refinement Type Checking via Assertion Checking. J. Inf. Process. Ryosuke Sato, Kazuyuki Asada, Naoki Kobayashi
2015	J	`jnl`	Verification of tree-processing programs via higher-order mode checking. Math. Struct. Comput. Sci. Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi
2015	C	`conf`	Verifying Relational Properties of Functional Programs by First-Order Refinement. PEPM Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi
2014	B	`conf`	A ZDD-Based Efficient Higher-Order Model Checking Algorithm. APLAS Taku Terao, Naoki Kobayashi
2014	A	`conf`	Automatic Termination Verification for Higher-Order Functional Programs. ESOP Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi
2014	B	`conf`	Complexity of Model-Checking Call-by-Value Programs. FoSSaCS Takeshi Tsukada, Naoki Kobayashi
2014	—	`ed.`	Concurrent Objects and Beyond - Papers dedicated to Akinori Yonezawa on the Occasion of His 65th Birthday Concurrent Objects and Beyond Gul A. Agha, Atsushi Igarashi, Naoki Kobayashi, Hidehiko Masuhara, Satoshi Matsuoka, Etsuya Shibayama, Kenjiro Taura
2014	B	`conf`	Deadlock Analysis of Unbounded Process Networks. CONCUR Elena Giachino, Naoki Kobayashi, Cosimo Laneve
2014	B	`conf`	Efficient Algorithm and Coding for Higher-Order Compression. DCC Kazuya Yaguchi, Naoki Kobayashi, Ayumi Shinohara
2014	—	`conf`	From Linear Types to Behavioural Types and Model Checking. Concurrent Objects and Beyond Naoki Kobayashi
2014	B	`conf`	Pairwise Reachability Analysis for Higher Order Concurrent Programs by Higher-Order Model Checking. CONCUR Kazuhide Yasukata, Naoki Kobayashi, Kazutaka Matsuda
2014	B	`conf`	Unsafe Order-2 Tree Languages Are Context-Sensitive. FoSSaCS Naoki Kobayashi, Kazuhiro Inaba, Takeshi Tsukada
2013	A*	`conf`	Automating relatively complete verification of higher-order functional programs. POPL Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi
2013	J	`jnl`	Model Checking Higher-Order Programs. J. ACM Naoki Kobayashi
2013	A	`conf`	Model-Checking Higher-Order Programs with Recursive Types. ESOP Naoki Kobayashi, Atsushi Igarashi
2013	B	`conf`	Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes. APLAS Koichi Fujima, Sohei Ito, Naoki Kobayashi
2013	A*	`conf`	Pumping by Typing. LICS Naoki Kobayashi
2013	B	`conf`	Saturation-Based Model Checking of Higher-Order Recursion Schemes. CSL Christopher H. Broadbent, Naoki Kobayashi
2013	C	`conf`	Towards a scalable software model checker for higher-order programs. PEPM Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi
2012	—	`conf`	An Intersection Type System for Deterministic Pushdown Automata. IFIP TCS Takeshi Tsukada, Naoki Kobayashi
2012	Misc	`conf`	Exact Flow Analysis by Higher-Order Model Checking. FLOPS Yoshihiro Tobita, Takeshi Tsukada, Naoki Kobayashi
2012	C	`conf`	Functional programs as compressed data. PEPM Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara
2012	J	`jnl`	Functional programs as compressed data. High. Order Symb. Comput. Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara, Kazuya Yaguchi
2012	B	`conf`	Program Certification by Higher-Order Model Checking. CPP Naoki Kobayashi
2011	B	`conf`	A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes. FoSSaCS Naoki Kobayashi
2011	J	`jnl`	Automated Techniques for Higher-Order Program Verification (NII Shonan Meeting 2011-5). NII Shonan Meet. Rep. Naoki Kobayashi, Luke Ong, David Van Horn
2011	J	`jnl`	Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus Log. Methods Comput. Sci. Naoki Kobayashi, C.-H. Luke Ong
2011	J	`jnl`	Environmental bisimulations for higher-order languages. ACM Trans. Program. Lang. Syst. Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii
2011	A*	`conf`	Higher-Order Model Checking: From Theory to Practice. LICS Naoki Kobayashi
2011	J	`jnl`	Ordered Types for Stream Processing of Tree-Structured Data. Inf. Media Technol. Ryosuke Sato, Kohei Suenaga, Naoki Kobayashi
2011	J	`jnl`	Ordered Types for Stream Processing of Tree-Structured Data. J. Inf. Process. Ryosuke Sato, Kohei Suenaga, Naoki Kobayashi
2011	A*	`conf`	Predicate abstraction and CEGAR for higher-order model checking. PLDI Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno
2011	B	`conf`	Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols. ATVA Morten Dahl, Naoki Kobayashi, Yunde Sun, Hans Hüttel
2010	J	`jnl`	A hybrid type system for lock-freedom of mobile processes. ACM Trans. Program. Lang. Syst. Naoki Kobayashi, Davide Sangiorgi
2010	Misc	`ed.`	Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings FLOPS Matthias Blume, Naoki Kobayashi, Germán Vidal
2010	A*	`conf`	Higher-order multi-parameter tree transducers and recursion schemes for program verification. POPL Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno
2010	B	`conf`	Untyped Recursion Schemes and Infinite Intersection Types. FoSSaCS Takeshi Tsukada, Naoki Kobayashi
2010	B	`conf`	Verification of Tree-Processing Programs via Higher-Order Model Checking. APLAS Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi
2009	A*	`conf`	A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes. LICS Naoki Kobayashi, C.-H. Luke Ong
2009	—	`conf`	Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus. ICALP (2) Naoki Kobayashi, C.-H. Luke Ong
2009	C	`conf`	Dependent type inference with interpolants. PPDP Hiroshi Unno, Naoki Kobayashi
2009	B	`conf`	Fractional Ownerships for Safe Memory Deallocation. APLAS Kohei Suenaga, Naoki Kobayashi
2009	—	`conf`	Higher-Order Program Verification and Language-Based Security. ASIAN Naoki Kobayashi
2009	C	`conf`	Model-checking higher-order functions. PPDP Naoki Kobayashi
2009	A	`conf`	Type-Based Automated Verification of Authenticity in Cryptographic Protocols. ESOP Daisuke Kikuchi, Naoki Kobayashi
2009	B	`conf`	Types and Recursion Schemes for Higher-Order Program Verification. APLAS Naoki Kobayashi
2009	A*	`conf`	Types and higher-order recursion schemes for verification of higher-order programs. POPL Naoki Kobayashi
2009	J	`jnl`	Undecidable equivalences for basic parallel processes. Inf. Comput. Hans Hüttel, Naoki Kobayashi, Takashi Suto
2008	A*	`conf`	A Hybrid Type System for Lock-Freedom of Mobile Processes. CAV Naoki Kobayashi, Davide Sangiorgi
2008	J	`jnl`	A New Type System for JVM Lock Primitives. New Gener. Comput. Futoshi Iwama, Naoki Kobayashi
2008	A	`conf`	Linear Declassification. ESOP Yûta Kaneko, Naoki Kobayashi
2008	Misc	`conf`	On-Demand Refinement of Dependent Types. FLOPS Hiroshi Unno, Naoki Kobayashi
2008	Misc	`conf`	Substructural Type Systems for Program Analysis. FLOPS Naoki Kobayashi
2008	J	`jnl`	Translation of tree-processing programs into stream-processing programs based on ordered linear type. J. Funct. Program. Koichi Kodama, Kohei Suenaga, Naoki Kobayashi
2008	—	`conf`	Tree Automata for Non-linear Arithmetic. RTA Naoki Kobayashi, Hitoshi Ohsaki
2007	A*	`conf`	Environmental Bisimulations for Higher-Order Languages. LICS Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii
2007	—	`conf`	Logical Bisimulations and Functional Languages. FSEN Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii
2007	—	`conf`	On the Complexity of Termination Inference for Processes. TGC Romain Demangeon, Daniel Hirschkoff, Naoki Kobayashi, Davide Sangiorgi
2007	A	`conf`	Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts. ESOP Kohei Suenaga, Naoki Kobayashi
2007	B	`conf`	Type-Based Verification of Correspondence Assertions for Communication Protocols. APLAS Daisuke Kikuchi, Naoki Kobayashi
2007	A*	`conf`	Undecidability of 2-Label BPP Equivalences and Behavioral Type Systems for the ICALP Naoki Kobayashi, Takashi Suto
2006	B	`conf`	A New Type System for Deadlock-Free Processes. CONCUR Naoki Kobayashi
2006	—	`conf`	Combining type-based analysis and model checking for finding counterexamples against non-interference. PLAS Hiroshi Unno, Naoki Kobayashi, Akinori Yonezawa
2006	B	`ed.`	Programming Languages and Systems, 4th Asian Symposium, APLAS 2006, Sydney, Australia, November 8-10, 2006, Proceedings APLAS Naoki Kobayashi
2006	B	`conf`	Resource Usage Analysis for the VMCAI Naoki Kobayashi, Kohei Suenaga, Lucian Wischik
2006	J	`jnl`	Resource Usage Analysis for the Pi-Calculus CoRR Naoki Kobayashi, Kohei Suenaga, Lucian Wischik
2006	J	`jnl`	Resource Usage Analysis for the p-Calculus. Log. Methods Comput. Sci. Naoki Kobayashi, Kohei Suenaga, Lucian Wischik
2006	C	`conf`	Resource usage analysis for a functional language with exceptions. PEPM Futoshi Iwama, Atsushi Igarashi, Naoki Kobayashi
2005	C	`conf`	Extension of Type-Based Approach to Generation of Stream-Processing Programs by Automatic Insertion of Buffering Primitives. LOPSTR Kohei Suenaga, Naoki Kobayashi, Akinori Yonezawa
2005	J	`jnl`	Resource usage analysis. ACM Trans. Program. Lang. Syst. Atsushi Igarashi, Naoki Kobayashi
2005	J	`jnl`	Type-based information flow analysis for the pi-calculus. Acta Informatica Naoki Kobayashi
2004	—	`conf`	A Coq Library for Verification of Concurrent Programs. LFM@IJCAR Reynald Affeldt, Naoki Kobayashi
2004	J	`jnl`	A generic type system for the Pi-calculus. Theor. Comput. Sci. Atsushi Igarashi, Naoki Kobayashi
2004	—	`conf`	Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes. EXPRESS Reynald Affeldt, Naoki Kobayashi
2004	B	`conf`	Region-Based Memory Management for a Dynamically-Typed Language. APLAS Akihito Nagata, Naoki Kobayashi, Akinori Yonezawa
2004	B	`conf`	Translation of Tree-Processing Programs into Stream-Processing Programs Based on Ordered Linear Type. APLAS Koichi Kodama, Kohei Suenaga, Naoki Kobayashi
2003	J	`jnl`	Information and Computation special issue from TACS 2001. Inf. Comput. Naoki Kobayashi, Benjamin C. Pierce
2003	—	`conf`	Time regions and effects for resource usage analysis. TLDI Naoki Kobayashi
2003	B	`conf`	Useless Code Elimination and Programm Slicing for the Pi-Calculus. APLAS Naoki Kobayashi
2002	J	`jnl`	A Type System for Lock-Free Processes. Inf. Comput. Naoki Kobayashi
2002	—	`conf`	A new type system for JVM lock primitives. ASIA-PEPM Futoshi Iwama, Naoki Kobayashi
2002	—	`conf`	AnZenMail: A Secure and Certified E-mail System. ISSS Etsuya Shibayama, Shigeki Hagihara, Naoki Kobayashi, Shin-ya Nishizaki, Kenjiro Taura, Takuo Watanabe
2002	—	`conf`	Formalization and Verification of a Mail Server in Coq. ISSS Reynald Affeldt, Naoki Kobayashi
2002	A*	`conf`	Resource usage analysis. POPL Atsushi Igarashi, Naoki Kobayashi
2002	—	`conf`	Type Systems for Concurrent Programs. 10th Anniversary Colloquium of UNU/IIST Naoki Kobayashi
2002	B	`conf`	Type-Based Information Analysis for Low-Level Languages. APLAS Naoki Kobayashi, Keita Shirane
2001	J	`jnl`	A Hybrid Approach to Online and Offline Partial Evaluation. High. Order Symb. Comput. Eijiro Sumii, Naoki Kobayashi
2001	A*	`conf`	A generic type system for the Pi-calculus. POPL Atsushi Igarashi, Naoki Kobayashi
2001	B	`conf`	Resource Usage Analysis. APLAS Atsushi Igarashi, Naoki Kobayashi
2001	—	`ed.`	Theoretical Aspects of Computer Software, 4th International Symposium, TACS 2001, Sendai, Japan, October 29-31, 2001, Proceedings TACS Naoki Kobayashi, Benjamin C. Pierce
2001	J	`jnl`	Type-Based Useless-Variable Elimination. High. Order Symb. Comput. Naoki Kobayashi
2000	B	`conf`	An Implicitly-Typed Deadlock-Free Process Calculus. CONCUR Naoki Kobayashi, Shin Saito, Eijiro Sumii
2000	C	`conf`	Online-and-Offline Partial Evaluation: A Mixed Approach (Extended Abstract). PEPM Eijiro Sumii, Naoki Kobayashi
2000	J	`jnl`	Type Reconstruction for Linear -Calculus with I/O Subtyping. Inf. Comput. Atsushi Igarashi, Naoki Kobayashi
2000	—	`conf`	Type Systems for Concurrent Processes: From Deadlock-Freedom to Livelock-Freedom, Time-Boundedness. IFIP TCS Naoki Kobayashi
2000	C	`conf`	Type-Based Useless Variable Elimination. PEPM Naoki Kobayashi
1999	J	`jnl`	Distributed Concurrent Linear Logic Programming. Theor. Comput. Sci. Naoki Kobayashi, Toshihiro Shimizu, Akinori Yonezawa
1999	—	`conf`	Distributed and concurrent objects based on linear logic (Invited Talk). FMOODS Naoki Kobayashi, Akinori Yonezawa
1999	J	`jnl`	Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst. Naoki Kobayashi, Benjamin C. Pierce, David N. Turner
1999	A*	`conf`	Quasi-Linear Types. POPL Naoki Kobayashi
1998	—	`conf`	A Generalized Deadlock-Free Process Calculus. HLCL Eijiro Sumii, Naoki Kobayashi
1998	J	`jnl`	A Partially Deadlock-Free Typed Process Calculus. ACM Trans. Program. Lang. Syst. Naoki Kobayashi
1998	—	`conf`	Type-Based Analysis of Concurrent Programs. Types in Compilation Naoki Kobayashi
1997	A*	`conf`	A Partially Deadlock-Free Typed Process Calculus. LICS Naoki Kobayashi
1997	B	`conf`	Type-Based Analysis of Communication for Concurrent Programming Languages. SAS Atsushi Igarashi, Naoki Kobayashi
1996	A*	`conf`	Linearity and the Pi-Calculus. POPL Naoki Kobayashi, Benjamin C. Pierce, David N. Turner
1996	—	`conf`	Partial Evaluation Scheme for Concurrent Languages and Its Correctness. Euro-Par, Vol. I Haruo Hosoya, Naoki Kobayashi, Akinori Yonezawa
1995	J	`jnl`	Asynchronous Communication Model Based on Linear Logic. Formal Aspects Comput. Naoki Kobayashi, Akinori Yonezawa
1995	B	`conf`	Static Analysis of Communication for Asynchronous Concurrent Programming Languages SAS Naoki Kobayashi, Motoki Nakade, Akinori Yonezawa
1995	J	`jnl`	Towards Foundations of Concurrent Object-Oriented Programming-Types and Language Design. Theory Pract. Object Syst. Naoki Kobayashi, Akinori Yonezawa
1994	—	`conf`	Higher-Order Concurrent Linear Logic Programming. Theory and Practice of Parallel Programming Naoki Kobayashi, Akinori Yonezawa
1994	—	`conf`	PARCS: An MPP-Oriented CLP Language. PASCO Kazuhiro Konno, Masaaki Nagatsuka, Naoki Kobayashi, Satoshi Matsuoka, Akinori Yonezawa
1994	A	`conf`	Type-Theoretic Foundations for Concurrent Object-Oriented Programming. OOPSLA Naoki Kobayashi, Akinori Yonezawa
1993	—	`conf`	ACL - A Concurrent Linear Logic Programming Paradigm. ILPS Naoki Kobayashi, Akinori Yonezawa
1992	—	`conf`	Asynchronous Communication Model Based on Linear Logic. Parallel Symbolic Computing Naoki Kobayashi, Akinori Yonezawa