# Naoki Kobayashi

According to our database

^{1}, Naoki Kobayashi## Timeline

#### Legend:

Book In proceedings Article PhD thesis Other## Links

#### Homepage:

#### On csauthors.net:

## Bibliography

2017

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

Sci. Comput. Program., 2017

Deadlock analysis of unbounded process networks.

Inf. Comput., 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

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

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

CoRR, 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.

Mathematical Structures in Computer Science, 2015

Refinement Type Checking via Assertion Checking.

JIP, 2015

Verifying Relational Properties of Functional Programs by First-Order Refinement.

Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, 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.

Higher-Order and Symbolic Computation, 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

Ordered Types for Stream Processing of Tree-Structured Data.

JIP, 2011

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

Logical Methods in Computer Science, 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

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

Proceedings of the Automata, Languages and Programming, 36th Internatilonal Colloquium, 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 Generation 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.

Electr. 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

A Hybrid Type System for Lock-Freedom of Mobile Processes.

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007

On the Complexity of Termination Inference for Processes.

Proceedings of the Trustworthy Global Computing, Third Symposium, 2007

Environmental Bisimulations for Higher-Order Languages.

Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 2007

Undecidability of 2-Label BPP Equivalences and Behavioral Type Systems for the

*pi*-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.

Logical Methods in Computer Science, 2006

Resource Usage Analysis for the Pi-Calculus

CoRR, 2006

Resource Usage Analysis for the

*pi*-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

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

Electr. Notes Theor. Comput. Sci., 2005

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

Acta Inf., 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

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

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

Translation of Tree-Processing Programs into Stream-Processing Programs Based on Ordered Linear Type.

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

Resource usage analysis.

Proceedings of the Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002

A new type system for JVM lock primitives.

Proceedings of the ACM SIGPLAN ASIA-PEPM 2002, 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.

Higher-Order and Symbolic Computation, 2001

Type-Based Useless-Variable Elimination.

Higher-Order and Symbolic Computation, 2001

A generic type system for the Pi-calculus.

Proceedings of the Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2001

Resource Usage Analysis.

Proceedings of the Second Asian Workshop on Programming Languages and Systems, 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-Based Useless Variable Elimination.

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

An Implicitly-Typed Deadlock-Free Process Calculus.

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

A Generalized Deadlock-Free Process Calculus.

Electr. 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

A Partially Deadlock-Free Typed Process Calculus.

Proceedings of the Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29, 1997

1996

Linearity and the Pi-Calculus.

Proceedings of the Conference Record of POPL'96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 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.

TAPOS, 1995

Asynchronous Communication Model Based on Linear Logic.

Formal Asp. 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 OOPSLA'94, 1994

1993

ACL - A Concurrent Linear Logic Programming Paradigm.

Proceedings of the Logic Programming, 1993

1992

Asynchronous Communication Model Based on Linear Logic.

Proceedings of the Parallel Symbolic Computing: Languages, 1992