Naoki Kobayashi

220 papers A* 22A 13B 55C 13Misc 5Journal 67Unranked 38
YearRankTypeTitle / 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