Naoki Kobayashi

According to our database, Naoki Kobayashi authored at least 166 papers between 1993 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2024

Asynchronous unfold/fold transformation for fixpoint logic.

Mahmudul Faisal Al Ameen, Naoki Kobayashi, Ryosuke Sato

Sci. Comput. Program., January, 2024

Borrowable Fractional Ownership Types for Verification.

Takashi Nakayama, Yusuke Matsushita, Ken Sakayori, Ryosuke Sato, Naoki Kobayashi

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2024

Ownership Types for Verification of Programs with Pointer Arithmetic.

Izumi Tanaka, Ken Sakayori, Naoki Kobayashi

Proceedings of the 2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation, 2024

Productivity Verification for Functional Programs by Reduction to Termination Verification.

Ren Fukaishi, Naoki Kobayashi, Ryosuke Sato

Proceedings of the 2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation, 2024

Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem.

Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato

Proceedings of the Programming Languages and Systems - 22nd Asian Symposium, 2024

2023

Higher-Order Property-Directed Reachability.

Hiroyuki Katsura, Naoki Kobayashi, Ryosuke Sato

Proc. ACM Program. Lang., August, 2023

HFL(Z) Validity Checking for Automated Program Verification.

Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, Takeshi Tsukada

Proc. ACM Program. Lang., January, 2023

Neural Network-Guided Synthesis of Recursive List Functions.

Naoki Kobayashi, Minchao Wu

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Gradual Tensor Shape Checking.

Momoko Hattori, Naoki Kobayashi, Ryosuke Sato

Proceedings of the Programming Languages and Systems, 2023

Argument Reduction of Constrained Horn Clauses Using Equality Constraints.

Ryo Ikeda, Ryosuke Sato, Naoki Kobayashi

Proceedings of the Programming Languages and Systems - 21st Asian Symposium, 2023

2022

Automatic HFL(Z) Validity Checking for Program Verification.

Kento Tanahashi, Naoki Kobayashi, Ryosuke Sato

CoRR, 2022

Parameterized Recursive Refinement Types for Automated Program Verification.

Ryoya Mukai, Naoki Kobayashi, Ryosuke Sato

Proceedings of the Static Analysis - 29th International Symposium, 2022

On Higher-Order Reachability Games Vs May Reachability.

Kazuyuki Asada, Hiroyuki Katsura, Naoki Kobayashi

Proceedings of the Reachability Problems - 16th International Conference, 2022

2021

Symbolic Automatic Relations and Their Applications to SMT and CHC Solving.

Takumi Shimoda, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato

Dataset, July, 2021

RustHorn: CHC-based Verification for Rust Programs.

Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi

ACM Trans. Program. Lang. Syst., 2021

A Probabilistic Higher-order Fixpoint Logic.

Yo Mitani, Naoki Kobayashi, Takeshi Tsukada

Log. Methods Comput. Sci., 2021

An Overview of the HFL Model Checking Project.

Naoki Kobayashi

Proceedings of the Proceedings 8th Workshop on Horn Clauses for Verification and Synthesis, 2021

Termination Analysis for the π-Calculus by Reduction to Sequential Program Termination.

Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada

CoRR, 2021

Symbolic Automatic Relations and Their Applications to SMT and CHC Solving.

Takumi Shimoda, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato

Proceedings of the Static Analysis - 28th International Symposium, 2021

Toward Neural-Network-Guided Program Synthesis and Verification.

Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno

Proceedings of the Static Analysis - 28th International Symposium, 2021

Counterexample generation for program verification based on ownership refinement types.

Hideto Ueno, John Toman, Naoki Kobayashi, Takeshi Tsukada

Proceedings of the 2021 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2021

Inside-Outside Algorithm for Macro Grammars.

Ryuta Kambe, Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara, Ryo Yoshinaka

Proceedings of the 15th International Conference on Grammatical Inference, 2021

A Cyclic Proof System for HFL_ℕ.

Mayuko Kori, Takeshi Tsukada, Naoki Kobayashi

Proceedings of the 29th EACSL Annual Conference on Computer Science Logic, 2021

Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes.

Patrick Baillot, Alexis Ghyselen, Naoki Kobayashi

Proceedings of the 32nd International Conference on Concurrency Theory, 2021

Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination.

Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada

Proceedings of the Programming Languages and Systems - 19th Asian Symposium, 2021

2020

On the Termination Problem for Probabilistic Higher-Order Recursive Programs.

Naoki Kobayashi, Ugo Dal Lago, Charles Grellois

Log. Methods Comput. Sci., 2020

ICE-Based Refinement Type Discovery for Higher-Order Functional Programs.

Adrien Champion, Tomoya Chiba, Naoki Kobayashi, Ryosuke Sato

J. Autom. Reason., 2020

A Cyclic Proof System for HFLN.

Mayuko Kori, Takeshi Tsukada, Naoki Kobayashi

CoRR, 2020

RustHorn: CHC-based Verification for Rust Programs (full version).

Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi

CoRR, 2020

Fold/Unfold Transformations for Fixpoint Logic.

Naoki Kobayashi, Grigory Fedyukovich, Aarti Gupta

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

Predicate Abstraction and CEGAR for $\nu \mathrm {HFL}_\mathbb {Z}$ Validity Checking.

Naoki Iwayama, Naoki Kobayashi, Ryota Suzuki, Takeshi Tsukada

Proceedings of the Static Analysis - 27th International Symposium, 2020

On Average-Case Hardness of Higher-Order Model Checking.

Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada

Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars.

Kazuyuki Asada, Naoki Kobayashi

Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs.

John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, Naoki Kobayashi

Proceedings of the Programming Languages and Systems, 2020

Grammar Compression with Probabilistic Context-Free Grammar.

Hiroaki Naganuma, Diptarama Hendrian, Ryo Yoshinaka, Ayumi Shinohara, Naoki Kobayashi

Proceedings of the Data Compression Conference, 2020

A New Refinement Type System for Automated $\nu \text {HFL}_\mathbb {Z}$ Validity Checking.

Hiroyuki Katsura, Naoki Iwayama, Naoki Kobayashi, Takeshi Tsukada

Proceedings of the Programming Languages and Systems - 18th Asian Symposium, 2020

2019

Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable.

Naoki Kobayashi

Theor. Comput. Sci., 2019

Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence.

Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada

Log. Methods Comput. Sci., 2019

A Temporal Logic for Higher-Order Functional Programs.

Yuya Okuyama, Takeshi Tsukada, Naoki Kobayashi

Proceedings of the Static Analysis - 26th International Symposium, 2019

Temporal Verification of Programs via First-Order Fixpoint Logic.

Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, Hiroshi Unno

Proceedings of the Static Analysis - 26th International Symposium, 2019

10 Years of the Higher-Order Model Checking Project (Extended Abstract).

Naoki Kobayashi

Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, 2019

Reduction from branching-time property verification of higher-order programs to HFL validity checking.

Keiichi Watanabe, Takeshi Tsukada, Hiroki Oshikawa, Naoki Kobayashi

Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2019

Combining higher-order model checking with refinement type inference.

Ryosuke Sato, Naoki Iwayama, Naoki Kobayashi

Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2019

A Type-Based HFL Model Checking Algorithm.

Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada

Proceedings of the Programming Languages and Systems - 17th Asian Symposium, 2019

2018

Special issue for the 42nd International Colloquium on Automata, Languages and Programming, ICALP 2015, Kyoto, Japan.

Magnús M. Halldórsson, Naoki Kobayashi, Bettina Speckmann

Inf. Comput., 2018

Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered.

Kazuyuki Asada, Naoki Kobayashi

Proceedings of the 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2018

Higher-Order Program Verification via HFL Model Checking.

Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe

Proceedings of the Programming Languages and Systems, 2018

Automated Synthesis of Functional Programs with Auxiliary Functions.

Shingo Eguchi, Naoki Kobayashi, Takeshi Tsukada

Proceedings of the Programming Languages and Systems - 16th Asian Symposium, 2018

HoIce: An ICE-Based Non-linear Horn Clause Solver.

Adrien Champion, Naoki Kobayashi, Ryosuke Sato

Proceedings of the Programming Languages and Systems - 16th Asian Symposium, 2018

2017

Verifying relational properties of functional programs by first-order refinement.

Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi

Sci. Comput. Program., 2017

Deadlock analysis of unbounded process networks.

Naoki Kobayashi, Cosimo Laneve

Inf. Comput., 2017

Streett Automata Model Checking of Higher-Order Recursion Schemes.

Ryota Suzuki, Koichi Fujima, Naoki Kobayashi, Takeshi Tsukada

Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, 2017

On the relationship between higher-order recursion schemes and higher-order fixpoint logic.

Naoki Kobayashi, Étienne Lozes, Florian Bruse

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Verification of code generators via higher-order model checking.

Takashi Suwa, Takeshi Tsukada, Naoki Kobayashi, Atsushi Igarashi

Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2017

Pumping Lemma for Higher-order Languages.

Kazuyuki Asada, Naoki Kobayashi

Proceedings of the 44th International Colloquium on Automata, Languages, and Programming, 2017

Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence.

Ryoma Sin'ya, Kazuyuki Asada, Naoki Kobayashi, Takeshi Tsukada

Proceedings of the Foundations of Software Science and Computation Structures, 2017

Modular Verification of Higher-Order Functional Programs.

Ryosuke Sato, Naoki Kobayashi

Proceedings of the Programming Languages and Systems, 2017

2016

Higher-Order Model Checking (NII Shonan Meeting 2016-4).

Naoki Kobayashi, Luke Ong, Igor Walukiewicz

NII Shonan Meet. Rep., 2016

Temporal verification of higher-order functional programs.

Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Automatically disproving fair termination of higher-order functional programs.

Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, Naoki Kobayashi

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

Compact bit encoding schemes for simply-typed lambda-terms.

Kotaro Takeda, Naoki Kobayashi, Kazuya Yaguchi, Ayumi Shinohara

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

On Word and Frontier Languages of Unsafe Higher-Order Grammars.

Kazuyuki Asada, Naoki Kobayashi

Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming, 2016

Equivalence-Based Abstraction Refinement for \mu HORS Model Checking.

Xin Li, Naoki Kobayashi

Proceedings of the Automated Technology for Verification and Analysis, 2016

Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation.

Kazuhide Yasukata, Takeshi Tsukada, Naoki Kobayashi

Proceedings of the Programming Languages and Systems - 14th Asian Symposium, 2016

Higher-Order Model Checking in Direct Style.

Taku Terao, Takeshi Tsukada, Naoki Kobayashi

Proceedings of the Programming Languages and Systems - 14th Asian Symposium, 2016

2015

Verification of tree-processing programs via higher-order mode checking.

Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi

Math. Struct. Comput. Sci., 2015

Refinement Type Checking via Assertion Checking.

Ryosuke Sato, Kazuyuki Asada, Naoki Kobayashi

J. Inf. Process., 2015

Automata-Based Abstraction Refinement for µHORS Model Checking.

Naoki Kobayashi, Xin Li

Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs.

Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs.

Yuma Matsumoto, Naoki Kobayashi, Hiroshi Unno

Proceedings of the Programming Languages and Systems - 13th Asian Symposium, 2015

Decision Algorithms for Checking Definability of Order-2 Finitary PCF.

Sadaaki Kawata, Kazuyuki Asada, Naoki Kobayashi

Proceedings of the Programming Languages and Systems - 13th Asian Symposium, 2015

2014

Complexity of Model-Checking Call-by-Value Programs.

Takeshi Tsukada, Naoki Kobayashi

Proceedings of the Foundations of Software Science and Computation Structures, 2014

Unsafe Order-2 Tree Languages Are Context-Sensitive.

Naoki Kobayashi, Kazuhiro Inaba, Takeshi Tsukada

Proceedings of the Foundations of Software Science and Computation Structures, 2014

Automatic Termination Verification for Higher-Order Functional Programs.

Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi

Proceedings of the Programming Languages and Systems, 2014

Efficient Algorithm and Coding for Higher-Order Compression.

Kazuya Yaguchi, Naoki Kobayashi, Ayumi Shinohara

Proceedings of the Data Compression Conference, 2014

Pairwise Reachability Analysis for Higher Order Concurrent Programs by Higher-Order Model Checking.

Kazuhide Yasukata, Naoki Kobayashi, Kazutaka Matsuda

Proceedings of the CONCUR 2014 - Concurrency Theory - 25th International Conference, 2014

Deadlock Analysis of Unbounded Process Networks.

Elena Giachino, Naoki Kobayashi, Cosimo Laneve

Proceedings of the CONCUR 2014 - Concurrency Theory - 25th International Conference, 2014

From Linear Types to Behavioural Types and Model Checking.

Naoki Kobayashi

Proceedings of the Concurrent Objects and Beyond, 2014

A ZDD-Based Efficient Higher-Order Model Checking Algorithm.

Taku Terao, Naoki Kobayashi

Proceedings of the Programming Languages and Systems - 12th Asian Symposium, 2014

2013

Model Checking Higher-Order Programs.

Naoki Kobayashi

J. ACM, 2013

Automating relatively complete verification of higher-order functional programs.

Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

Towards a scalable software model checker for higher-order programs.

Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi

Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, 2013

Pumping by Typing.

Naoki Kobayashi

Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

Model-Checking Higher-Order Programs with Recursive Types.

Naoki Kobayashi, Atsushi Igarashi

Proceedings of the Programming Languages and Systems, 2013

Saturation-Based Model Checking of Higher-Order Recursion Schemes.

Christopher H. Broadbent, Naoki Kobayashi

Proceedings of the Computer Science Logic 2013 (CSL 2013), 2013

Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes.

Koichi Fujima, Sohei Ito, Naoki Kobayashi

Proceedings of the Programming Languages and Systems - 11th Asian Symposium, 2013

2012

Functional programs as compressed data.

Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara, Kazuya Yaguchi

High. Order Symb. Comput., 2012

Functional programs as compressed data.

Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara

Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation, 2012

An Intersection Type System for Deterministic Pushdown Automata.

Takeshi Tsukada, Naoki Kobayashi

Proceedings of the Theoretical Computer Science, 2012

Exact Flow Analysis by Higher-Order Model Checking.

Yoshihiro Tobita, Takeshi Tsukada, Naoki Kobayashi

Proceedings of the Functional and Logic Programming - 11th International Symposium, 2012

Program Certification by Higher-Order Model Checking.

Naoki Kobayashi

Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

2011

Environmental bisimulations for higher-order languages.

Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii

ACM Trans. Program. Lang. Syst., 2011

Automated Techniques for Higher-Order Program Verification (NII Shonan Meeting 2011-5).

Naoki Kobayashi, Luke Ong, David Van Horn

NII Shonan Meet. Rep., 2011

Ordered Types for Stream Processing of Tree-Structured Data.

Ryosuke Sato, Kohei Suenaga, Naoki Kobayashi

J. Inf. Process., 2011

Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus

Naoki Kobayashi, C.-H. Luke Ong

Log. Methods Comput. Sci., 2011

Predicate abstraction and CEGAR for higher-order model checking.

Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno

Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011

Higher-Order Model Checking: From Theory to Practice.

Naoki Kobayashi

Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, 2011

A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes.

Naoki Kobayashi

Proceedings of the Foundations of Software Science and Computational Structures, 2011

Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols.

Morten Dahl, Naoki Kobayashi, Yunde Sun, Hans Hüttel

Proceedings of the Automated Technology for Verification and Analysis, 2011

2010

A hybrid type system for lock-freedom of mobile processes.

Naoki Kobayashi, Davide Sangiorgi

ACM Trans. Program. Lang. Syst., 2010

Higher-order multi-parameter tree transducers and recursion schemes for program verification.

Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno

Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Untyped Recursion Schemes and Infinite Intersection Types.

Takeshi Tsukada, Naoki Kobayashi

Proceedings of the Foundations of Software Science and Computational Structures, 2010

Verification of Tree-Processing Programs via Higher-Order Model Checking.

Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi

Proceedings of the Programming Languages and Systems - 8th Asian Symposium, 2010

2009

Undecidable equivalences for basic parallel processes.

Hans Hüttel, Naoki Kobayashi, Takashi Suto

Inf. Comput., 2009

Dependent type inference with interpolants.

Hiroshi Unno, Naoki Kobayashi

Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2009

Model-checking higher-order functions.

Naoki Kobayashi

Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2009

Types and higher-order recursion schemes for verification of higher-order programs.

Naoki Kobayashi

Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes.

Naoki Kobayashi, C.-H. Luke Ong

Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, 2009

Type-Based Automated Verification of Authenticity in Cryptographic Protocols.

Daisuke Kikuchi, Naoki Kobayashi

Proceedings of the Programming Languages and Systems, 2009

Higher-Order Program Verification and Language-Based Security.

Naoki Kobayashi

Proceedings of the Advances in Computer Science, 2009

Fractional Ownerships for Safe Memory Deallocation.

Kohei Suenaga, Naoki Kobayashi

Proceedings of the Programming Languages and Systems, 7th Asian Symposium, 2009

Types and Recursion Schemes for Higher-Order Program Verification.

Naoki Kobayashi

Proceedings of the Programming Languages and Systems, 7th Asian Symposium, 2009

2008

A New Type System for JVM Lock Primitives.

Futoshi Iwama, Naoki Kobayashi

New Gener. Comput., 2008

Translation of tree-processing programs into stream-processing programs based on ordered linear type.

Koichi Kodama, Kohei Suenaga, Naoki Kobayashi

J. Funct. Program., 2008

Tree Automata for Non-linear Arithmetic.

Naoki Kobayashi, Hitoshi Ohsaki

Proceedings of the Rewriting Techniques and Applications, 19th International Conference, 2008

On-Demand Refinement of Dependent Types.

Hiroshi Unno, Naoki Kobayashi

Proceedings of the Functional and Logic Programming, 9th International Symposium, 2008

Substructural Type Systems for Program Analysis.

Naoki Kobayashi

Proceedings of the Functional and Logic Programming, 9th International Symposium, 2008

Linear Declassification.

Yûta Kaneko, Naoki Kobayashi

Proceedings of the Programming Languages and Systems, 2008

2007

On the Complexity of Termination Inference for Processes.

Romain Demangeon, Daniel Hirschkoff, Naoki Kobayashi, Davide Sangiorgi

Proceedings of the Trustworthy Global Computing, Third Symposium, 2007

Undecidability of 2-Label BPP Equivalences and Behavioral Type Systems for the <i>pi</i> -Calculus.

Naoki Kobayashi, Takashi Suto

Proceedings of the Automata, Languages and Programming, 34th International Colloquium, 2007

Logical Bisimulations and Functional Languages.

Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii

Proceedings of the International Symposium on Fundamentals of Software Engineering, 2007

Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts.

Kohei Suenaga, Naoki Kobayashi

Proceedings of the Programming Languages and Systems, 2007

Type-Based Verification of Correspondence Assertions for Communication Protocols.

Daisuke Kikuchi, Naoki Kobayashi

Proceedings of the Programming Languages and Systems, 5th Asian Symposium, 2007

2006

Resource Usage Analysis for the p-Calculus.

Naoki Kobayashi, Kohei Suenaga, Lucian Wischik

Log. Methods Comput. Sci., 2006

Resource Usage Analysis for the Pi-Calculus

Naoki Kobayashi, Kohei Suenaga, Lucian Wischik

CoRR, 2006

Resource Usage Analysis for the <i>pi</i>-Calculus.

Naoki Kobayashi, Kohei Suenaga, Lucian Wischik

Proceedings of the Verification, 2006

Combining type-based analysis and model checking for finding counterexamples against non-interference.

Hiroshi Unno, Naoki Kobayashi, Akinori Yonezawa

Proceedings of the 2006 Workshop on Programming Languages and Analysis for Security, 2006

Resource usage analysis for a functional language with exceptions.

Futoshi Iwama, Atsushi Igarashi, Naoki Kobayashi

Proceedings of the 2006 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2006

A New Type System for Deadlock-Free Processes.

Naoki Kobayashi

Proceedings of the CONCUR 2006 - Concurrency Theory, 17th International Conference, 2006

2005

Resource usage analysis.

Atsushi Igarashi, Naoki Kobayashi

ACM Trans. Program. Lang. Syst., 2005

Type-based information flow analysis for the pi-calculus.

Naoki Kobayashi

Acta Informatica, 2005

Extension of Type-Based Approach to Generation of Stream-Processing Programs by Automatic Insertion of Buffering Primitives.

Kohei Suenaga, Naoki Kobayashi, Akinori Yonezawa

Proceedings of the Logic Based Program Synthesis and Transformation, 2005

2004

A generic type system for the Pi-calculus.

Atsushi Igarashi, Naoki Kobayashi

Theor. Comput. Sci., 2004

A Coq Library for Verification of Concurrent Programs.

Reynald Affeldt, Naoki Kobayashi

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages, 2004

Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes.

Reynald Affeldt, Naoki Kobayashi

Proceedings of the 11th International Workshop on Expressiveness in Concurrency, 2004

Region-Based Memory Management for a Dynamically-Typed Language.

Akihito Nagata, Naoki Kobayashi, Akinori Yonezawa

Proceedings of the Programming Languages and Systems: Second Asian Symposium, 2004

2003

Information and Computation special issue from TACS 2001.

Naoki Kobayashi, Benjamin C. Pierce

Inf. Comput., 2003

Time regions and effects for resource usage analysis.

Naoki Kobayashi

Proceedings of TLDI'03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2003

Useless Code Elimination and Programm Slicing for the Pi-Calculus.

Naoki Kobayashi

Proceedings of the Programming Languages and Systems, First Asian Symposium, 2003

2002

A Type System for Lock-Free Processes.

Naoki Kobayashi

Inf. Comput., 2002

Type Systems for Concurrent Programs.

Naoki Kobayashi

Proceedings of the Formal Methods at the Crossroads. From Panacea to Foundational Support, 2002

AnZenMail: A Secure and Certified E-mail System.

Etsuya Shibayama, Shigeki Hagihara, Naoki Kobayashi, Shin-ya Nishizaki, Kenjiro Taura, Takuo Watanabe

Proceedings of the Software Security -- Theories and Systems, 2002

Formalization and Verification of a Mail Server in Coq.

Reynald Affeldt, Naoki Kobayashi

Proceedings of the Software Security -- Theories and Systems, 2002

Type-Based Information Analysis for Low-Level Languages.

Naoki Kobayashi, Keita Shirane

Proceedings of the Third Asian Workshop on Programming Languages and Systems, 2002

2001

A Hybrid Approach to Online and Offline Partial Evaluation.

Eijiro Sumii, Naoki Kobayashi

High. Order Symb. Comput., 2001

Type-Based Useless-Variable Elimination.

Naoki Kobayashi

High. Order Symb. Comput., 2001

2000

Type Reconstruction for Linear -Calculus with I/O Subtyping.

Atsushi Igarashi, Naoki Kobayashi

Inf. Comput., 2000

Online-and-Offline Partial Evaluation: A Mixed Approach (Extended Abstract).

Eijiro Sumii, Naoki Kobayashi

Proceedings of the 2000 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '00), 2000

Type Systems for Concurrent Processes: From Deadlock-Freedom to Livelock-Freedom, Time-Boundedness.

Naoki Kobayashi

Proceedings of the Theoretical Computer Science, 2000

An Implicitly-Typed Deadlock-Free Process Calculus.

Naoki Kobayashi, Shin Saito, Eijiro Sumii

Proceedings of the CONCUR 2000, 2000

1999

Linearity and the pi-calculus.

Naoki Kobayashi, Benjamin C. Pierce, David N. Turner

ACM Trans. Program. Lang. Syst., 1999

Distributed Concurrent Linear Logic Programming.

Naoki Kobayashi, Toshihiro Shimizu, Akinori Yonezawa

Theor. Comput. Sci., 1999

Quasi-Linear Types.

Naoki Kobayashi

Proceedings of the POPL '99, 1999

Distributed and concurrent objects based on linear logic (Invited Talk).

Naoki Kobayashi, Akinori Yonezawa

Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 1999

1998

A Partially Deadlock-Free Typed Process Calculus.

Naoki Kobayashi

ACM Trans. Program. Lang. Syst., 1998

A Generalized Deadlock-Free Process Calculus.

Eijiro Sumii, Naoki Kobayashi

Proceedings of the 3rd International Workshop on High-Level Concurrent Languages, 1998

Type-Based Analysis of Concurrent Programs.

Naoki Kobayashi

Proceedings of the Types in Compilation, Second International Workshop, 1998

1997

Type-Based Analysis of Communication for Concurrent Programming Languages.

Atsushi Igarashi, Naoki Kobayashi

Proceedings of the Static Analysis, 4th International Symposium, 1997

1996

Partial Evaluation Scheme for Concurrent Languages and Its Correctness.

Haruo Hosoya, Naoki Kobayashi, Akinori Yonezawa

Proceedings of the Euro-Par '96 Parallel Processing, 1996

1995

Towards Foundations of Concurrent Object-Oriented Programming-Types and Language Design.

Naoki Kobayashi, Akinori Yonezawa

Theory Pract. Object Syst., 1995

Asynchronous Communication Model Based on Linear Logic.

Naoki Kobayashi, Akinori Yonezawa

Formal Aspects Comput., 1995

Static Analysis of Communication for Asynchronous Concurrent Programming Languages

Naoki Kobayashi, Motoki Nakade, Akinori Yonezawa

Proceedings of the Static Analysis, 1995

1994

Higher-Order Concurrent Linear Logic Programming.

Naoki Kobayashi, Akinori Yonezawa

Proceedings of the Theory and Practice of Parallel Programming, 1994

PARCS: An MPP-Oriented CLP Language.

Kazuhiro Konno, Masaaki Nagatsuka, Naoki Kobayashi, Satoshi Matsuoka, Akinori Yonezawa

Proceedings of the First International Symposium on Parallel Symbolic Computation, 1994

Type-Theoretic Foundations for Concurrent Object-Oriented Programming.

Naoki Kobayashi, Akinori Yonezawa

Proceedings of the Ninth Annual Conference on Object-Oriented Programming Systems, 1994

1993

ACL - A Concurrent Linear Logic Programming Paradigm.

Naoki Kobayashi, Akinori Yonezawa

Proceedings of the Logic Programming, 1993