# Naoki Kobayashi

Affiliations:
• Graduate School of Information Science and Technology, University of Tokyo, Japan

According to our database1, Naoki Kobayashi authored at least 154 papers between 1993 and 2022.

Collaborative distances:

Book
In proceedings
Article
PhD thesis
Other

## Bibliography

2022
On Higher-Order Reachability Games vs May Reachability.
CoRR, 2022

CoRR, 2022

Automatic HFL(Z) Validity Checking for Program Verification.
CoRR, 2022

Asynchronous Unfold/Fold Transformation for Fixpoint Logic.
Proceedings of the Functional and Logic Programming - 16th International Symposium, 2022

2021
RustHorn: CHC-based Verification for Rust Programs.
ACM Trans. Program. Lang. Syst., 2021

A Probabilistic Higher-order Fixpoint Logic.
Log. Methods Comput. Sci., 2021

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

Symbolic Automatic Relations and Their Applications to SMT and CHC Solving.
Proceedings of the Static Analysis - 28th International Symposium, 2021

Toward Neural-Network-Guided Program Synthesis and Verification.
Proceedings of the Static Analysis - 28th International Symposium, 2021

Counterexample generation for program verification based on ownership refinement types.
Proceedings of the 2021 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2021

Inside-Outside Algorithm for Macro Grammars.
Proceedings of the 15th International Conference on Grammatical Inference, 2021

A Cyclic Proof System for HFL_ℕ.
Proceedings of the 29th EACSL Annual Conference on Computer Science Logic, 2021

Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes.
Proceedings of the 32nd International Conference on Concurrency Theory, 2021

Termination Analysis for the $$\pi$$-Calculus by Reduction to Sequential Program Termination.
Proceedings of the Programming Languages and Systems - 19th Asian Symposium, 2021

2020
On the Termination Problem for Probabilistic Higher-Order Recursive Programs.
Log. Methods Comput. Sci., 2020

ICE-Based Refinement Type Discovery for Higher-Order Functional Programs.
J. Autom. Reason., 2020

A Cyclic Proof System for HFLN.
CoRR, 2020

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

Fold/Unfold Transformations for Fixpoint Logic.
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.
Proceedings of the Static Analysis - 27th International Symposium, 2020

On Average-Case Hardness of Higher-Order Model Checking.
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.
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.
Proceedings of the Programming Languages and Systems, 2020

Grammar Compression with Probabilistic Context-Free Grammar.
Proceedings of the Data Compression Conference, 2020

A New Refinement Type System for Automated $\nu \text {HFL}_\mathbb {Z}$ Validity Checking.
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.
Theor. Comput. Sci., 2019

Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence.
Log. Methods Comput. Sci., 2019

A Temporal Logic for Higher-Order Functional Programs.
Proceedings of the Static Analysis - 26th International Symposium, 2019

Temporal Verification of Programs via First-Order Fixpoint Logic.
Proceedings of the Static Analysis - 26th International Symposium, 2019

10 Years of the Higher-Order Model Checking Project (Extended Abstract).
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.
Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2019

Combining higher-order model checking with refinement type inference.
Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2019

A Type-Based HFL Model Checking Algorithm.
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.
Inf. Comput., 2018

Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered.
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.
Proceedings of the Programming Languages and Systems, 2018

Automated Synthesis of Functional Programs with Auxiliary Functions.
Proceedings of the Programming Languages and Systems - 16th Asian Symposium, 2018

HoIce: An ICE-Based Non-linear Horn Clause Solver.
Proceedings of the Programming Languages and Systems - 16th Asian Symposium, 2018

2017
Verifying relational properties of functional programs by first-order refinement.
Sci. Comput. Program., 2017

Deadlock analysis of unbounded process networks.
Inf. Comput., 2017

Streett Automata Model Checking of Higher-Order Recursion Schemes.
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.
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Verification of code generators via higher-order model checking.
Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2017

Pumping Lemma for Higher-order Languages.
Proceedings of the 44th International Colloquium on Automata, Languages, and Programming, 2017

Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence.
Proceedings of the Foundations of Software Science and Computation Structures, 2017

Modular Verification of Higher-Order Functional Programs.
Proceedings of the Programming Languages and Systems, 2017

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

Temporal verification of higher-order functional programs.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Automatically disproving fair termination of higher-order functional programs.
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

Compact bit encoding schemes for simply-typed lambda-terms.
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

On Word and Frontier Languages of Unsafe Higher-Order Grammars.
Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming, 2016

Equivalence-Based Abstraction Refinement for \mu HORS Model Checking.
Proceedings of the Automated Technology for Verification and Analysis, 2016

Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation.
Proceedings of the Programming Languages and Systems - 14th Asian Symposium, 2016

Higher-Order Model Checking in Direct Style.
Proceedings of the Programming Languages and Systems - 14th Asian Symposium, 2016

2015
Verification of tree-processing programs via higher-order mode checking.
Math. Struct. Comput. Sci., 2015

Refinement Type Checking via Assertion Checking.
J. Inf. Process., 2015

Automata-Based Abstraction Refinement for µHORS Model Checking.
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.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs.
Proceedings of the Programming Languages and Systems - 13th Asian Symposium, 2015

Decision Algorithms for Checking Definability of Order-2 Finitary PCF.
Proceedings of the Programming Languages and Systems - 13th Asian Symposium, 2015

2014
Complexity of Model-Checking Call-by-Value Programs.
Proceedings of the Foundations of Software Science and Computation Structures, 2014

Unsafe Order-2 Tree Languages Are Context-Sensitive.
Proceedings of the Foundations of Software Science and Computation Structures, 2014

Automatic Termination Verification for Higher-Order Functional Programs.
Proceedings of the Programming Languages and Systems, 2014

Efficient Algorithm and Coding for Higher-Order Compression.
Proceedings of the Data Compression Conference, 2014

Pairwise Reachability Analysis for Higher Order Concurrent Programs by Higher-Order Model Checking.
Proceedings of the CONCUR 2014 - Concurrency Theory - 25th International Conference, 2014

Deadlock Analysis of Unbounded Process Networks.
Proceedings of the CONCUR 2014 - Concurrency Theory - 25th International Conference, 2014

From Linear Types to Behavioural Types and Model Checking.
Proceedings of the Concurrent Objects and Beyond, 2014

A ZDD-Based Efficient Higher-Order Model Checking Algorithm.
Proceedings of the Programming Languages and Systems - 12th Asian Symposium, 2014

2013
Model Checking Higher-Order Programs.
J. ACM, 2013

Automating relatively complete verification of higher-order functional programs.
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.
Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, 2013

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

Model-Checking Higher-Order Programs with Recursive Types.
Proceedings of the Programming Languages and Systems, 2013

Saturation-Based Model Checking of Higher-Order Recursion Schemes.
Proceedings of the Computer Science Logic 2013 (CSL 2013), 2013

Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes.
Proceedings of the Programming Languages and Systems - 11th Asian Symposium, 2013

2012
Functional programs as compressed data.
High. Order Symb. Comput., 2012

Functional programs as compressed data.
Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation, 2012

An Intersection Type System for Deterministic Pushdown Automata.
Proceedings of the Theoretical Computer Science, 2012

Exact Flow Analysis by Higher-Order Model Checking.
Proceedings of the Functional and Logic Programming - 11th International Symposium, 2012

Program Certification by Higher-Order Model Checking.
Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

2011
Environmental bisimulations for higher-order languages.
ACM Trans. Program. Lang. Syst., 2011

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

Ordered Types for Stream Processing of Tree-Structured Data.
J. Inf. Process., 2011

Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus
Log. Methods Comput. Sci., 2011

Predicate abstraction and CEGAR for higher-order model checking.
Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011

Higher-Order Model Checking: From Theory to Practice.
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.
Proceedings of the Foundations of Software Science and Computational Structures, 2011

Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols.
Proceedings of the Automated Technology for Verification and Analysis, 2011

2010
A hybrid type system for lock-freedom of mobile processes.
ACM Trans. Program. Lang. Syst., 2010

Higher-order multi-parameter tree transducers and recursion schemes for program verification.
Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Untyped Recursion Schemes and Infinite Intersection Types.
Proceedings of the Foundations of Software Science and Computational Structures, 2010

Verification of Tree-Processing Programs via Higher-Order Model Checking.
Proceedings of the Programming Languages and Systems - 8th Asian Symposium, 2010

2009
Undecidable equivalences for basic parallel processes.
Inf. Comput., 2009

Dependent type inference with interpolants.
Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2009

Model-checking higher-order functions.
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.
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.
Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, 2009

Type-Based Automated Verification of Authenticity in Cryptographic Protocols.
Proceedings of the Programming Languages and Systems, 2009

Higher-Order Program Verification and Language-Based Security.
Proceedings of the Advances in Computer Science, 2009

Fractional Ownerships for Safe Memory Deallocation.
Proceedings of the Programming Languages and Systems, 7th Asian Symposium, 2009

Types and Recursion Schemes for Higher-Order Program Verification.
Proceedings of the Programming Languages and Systems, 7th Asian Symposium, 2009

2008
A New Type System for JVM Lock Primitives.
New Gener. Comput., 2008

Translation of tree-processing programs into stream-processing programs based on ordered linear type.
J. Funct. Program., 2008

A Coq Library for Verification of Concurrent Programs.
Electron. Notes Theor. Comput. Sci., 2008

Tree Automata for Non-linear Arithmetic.
Proceedings of the Rewriting Techniques and Applications, 19th International Conference, 2008

On-Demand Refinement of Dependent Types.
Proceedings of the Functional and Logic Programming, 9th International Symposium, 2008

Substructural Type Systems for Program Analysis.
Proceedings of the Functional and Logic Programming, 9th International Symposium, 2008

Linear Declassification.
Proceedings of the Programming Languages and Systems, 2008

2007
On the Complexity of Termination Inference for Processes.
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.
Proceedings of the Automata, Languages and Programming, 34th International Colloquium, 2007

Logical Bisimulations and Functional Languages.
Proceedings of the International Symposium on Fundamentals of Software Engineering, 2007

Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts.
Proceedings of the Programming Languages and Systems, 2007

Type-Based Verification of Correspondence Assertions for Communication Protocols.
Proceedings of the Programming Languages and Systems, 5th Asian Symposium, 2007

2006
Resource Usage Analysis for the p-Calculus.
Log. Methods Comput. Sci., 2006

Resource Usage Analysis for the Pi-Calculus
CoRR, 2006

Resource Usage Analysis for the <i>pi</i>-Calculus.
Proceedings of the Verification, 2006

Combining type-based analysis and model checking for finding counterexamples against non-interference.
Proceedings of the 2006 Workshop on Programming Languages and Analysis for Security, 2006

Resource usage analysis for a functional language with exceptions.
Proceedings of the 2006 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2006

A New Type System for Deadlock-Free Processes.
Proceedings of the CONCUR 2006 - Concurrency Theory, 17th International Conference, 2006

2005
Resource usage analysis.
ACM Trans. Program. Lang. Syst., 2005

Type-based information flow analysis for the pi-calculus.
Acta Informatica, 2005

Extension of Type-Based Approach to Generation of Stream-Processing Programs by Automatic Insertion of Buffering Primitives.
Proceedings of the Logic Based Program Synthesis and Transformation, 2005

2004
A generic type system for the Pi-calculus.
Theor. Comput. Sci., 2004

Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes.
Proceedings of the 11th International Workshop on Expressiveness in Concurrency, 2004

Region-Based Memory Management for a Dynamically-Typed Language.
Proceedings of the Programming Languages and Systems: Second Asian Symposium, 2004

2003
Information and Computation special issue from TACS 2001.
Inf. Comput., 2003

Time regions and effects for resource usage analysis.
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.
Proceedings of the Programming Languages and Systems, First Asian Symposium, 2003

2002
A Type System for Lock-Free Processes.
Inf. Comput., 2002

Type Systems for Concurrent Programs.
Proceedings of the Formal Methods at the Crossroads. From Panacea to Foundational Support, 2002

AnZenMail: A Secure and Certified E-mail System.
Proceedings of the Software Security -- Theories and Systems, 2002

Formalization and Verification of a Mail Server in Coq.
Proceedings of the Software Security -- Theories and Systems, 2002

Type-Based Information Analysis for Low-Level Languages.
Proceedings of the Third Asian Workshop on Programming Languages and Systems, 2002

2001
A Hybrid Approach to Online and Offline Partial Evaluation.
High. Order Symb. Comput., 2001

Type-Based Useless-Variable Elimination.
High. Order Symb. Comput., 2001

2000
Type Reconstruction for Linear -Calculus with I/O Subtyping.
Inf. Comput., 2000

Online-and-Offline Partial Evaluation: A Mixed Approach (Extended Abstract).
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.
Proceedings of the Theoretical Computer Science, 2000

Proceedings of the CONCUR 2000, 2000

1999
Linearity and the pi-calculus.
ACM Trans. Program. Lang. Syst., 1999

Distributed Concurrent Linear Logic Programming.
Theor. Comput. Sci., 1999

Quasi-Linear Types.
Proceedings of the POPL '99, 1999

Distributed and concurrent objects based on linear logic (Invited Talk).
Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 1999

1998
A Partially Deadlock-Free Typed Process Calculus.
ACM Trans. Program. Lang. Syst., 1998

Electron. Notes Theor. Comput. Sci., 1998

Type-Based Analysis of Concurrent Programs.
Proceedings of the Types in Compilation, Second International Workshop, 1998

1997
Type-Based Analysis of Communication for Concurrent Programming Languages.
Proceedings of the Static Analysis, 4th International Symposium, 1997

1996
Partial Evaluation Scheme for Concurrent Languages and Its Correctness.
Proceedings of the Euro-Par '96 Parallel Processing, 1996

1995
Towards Foundations of Concurrent Object-Oriented Programming-Types and Language Design.
Theory Pract. Object Syst., 1995

Asynchronous Communication Model Based on Linear Logic.
Formal Aspects Comput., 1995

Static Analysis of Communication for Asynchronous Concurrent Programming Languages
Proceedings of the Static Analysis, 1995

1994
Higher-Order Concurrent Linear Logic Programming.
Proceedings of the Theory and Practice of Parallel Programming, 1994

Type-Theoretic Foundations for Concurrent Object-Oriented Programming.
Proceedings of the Ninth Annual Conference on Object-Oriented Programming Systems, 1994

1993
ACL - A Concurrent Linear Logic Programming Paradigm.
Proceedings of the Logic Programming, 1993