Kobayashi, Koichiro, Ogasawara, Masahiro, Kiyama, Yoshio, Miyazono, Takayoshi, Kagawa, Kumiko, Imai, Kiyotoshi, ...
A 23-year old woman with acute biphenotypic leukemia (ABL) complained of chest pain with cough, high fever and hemoptysis during induction chemotherapy, although she had been treated with...
Logical Bisimulations and Functional Languages ⋆ (2008)
Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii
Abstract. Developing a theory of bisimulation in higher-order languages can be hard. Particularly challenging can be the proof of congruence and, related to this, enhancements of the bisimulation...
Maximum distributions of bridges of noncolliding Brownian paths (2008)
Kobayashi, Naoki, Izumi, Minami, Katori, Makoto
The one-dimensional Brownian motion starting from the origin at time $t=0$, conditioned to return to the origin at time $t=1$ and to stay positive during time interval $0 < t < 1$, is called the...
The trace equivalence of BPP was shown to be undecidable by Hirshfeld. We show that the trace equivalence remains undecidable even if the number of labels is restricted to two. The undecidability...
Type-Based Verification of Correspondence Assertions for Communication Protocols (2008)
Daisuke Kikuchi, Naoki Kobayashi
Abstract. Gordon and Jeffrey developed a type system for checking correspondence assertions. The correspondence assertions, proposed by Woo and Lam, state that when a certain event (called an “end...
Region-Based Memory Management for a Dynamically-Typed Language (2008)
Akihito Nagata, Naoki Kobayashi, Akinori Yonezawa
Abstract. Region-based memory management scheme has been proposed for programming language ML. In this scheme, a compiler statically estimates the live range of each object by performing an extension...
Limit distributions of two-dimensional quantum walks (2008)
Watabe, Kyohei, Kobayashi, Naoki, Katori, Makoto, Konno, Norio
One-parameter family of discrete-time quantum-walk models on the square lattice, which includes the Grover-walk model as a special case, is analytically studied. Convergence in the long-time limit $t...
Large Qudit Limit of One-dimensional Quantum Walks (2008)
Sato, Mitsunori, Kobayashi, Naoki, Katori, Makoto, Konno, Norio
We study a series of one-dimensional discrete-time quantum-walk models labeled by half integers $j=1/2, 1, 3/2, ...$, introduced by Miyazaki {\it et al.}, each of which the walker's wave function has...
Logical Bisimulations and functional languages ⋆ (2008)
Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii
Abstract. Developing a theory of bisimulation in higher-order languages can be hard. Particularly challenging can be the proof of congruence and, related to this, enhancements of the bisimulation...
Linear types (types of values that can be used just once) have been drawing a great deal of attention because they are useful for memory management, in-place update of data structures, etc.: an...
A Partially Deadlock-free Typed Process Calculus (I) -- A Simple System -- (2007)
Concurrency primitives play an important role in describing programs on parallel /distributed environments and also in writing interactive programs. Theoretical supports for concurrency primitives,...
Atsushi Igarashi, Naoki Kobayashi
It is an important criterion of program correctness that a program accesses resources in a valid manner. For example, a memory region that has been allocated should eventually be deallocated, and...
Katori, Makoto, Izumi, Minami, Kobayashi, Naoki
It is known that the moments of the maximum value of a one-dimensional conditional Brownian motion, the three-dimensional Bessel bridge with duration 1 started from the origin, are expressed using...
Equivalence between quantum simultaneous games and quantum sequential games (2007)
A framework for discussing relationships between different types of games is proposed. Within the framework, quantum simultaneous games, finite quantum simultaneous games, quantum sequential games,...
Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts (2007)
Kohei Suenaga, Naoki Kobayashi
Abstract. The goal of our research project is to establish a type-based method for verification of certain critical properties (such as deadlockand race-freedom) of operating system kernels. As...
Resource Usage Analysis for the Pi-Calculus (2006)
Kobayashi, Naoki, Suenaga, Kohei, Wischik, Lucian
We propose a type-based resource usage analysis for the π-calculus extended with resource creation/access primitives. The goal of the resource usage analysis is to statically check that a...
Mapping of panda plumage color locus on the microsatellite linkage map of the Japanese quail (2006)
Miwa, Mitsuru, Inoue-Murayama, Miho, Kobayashi, Naoki, Kayang, Boniface, Mizutani, Makoto, Takahashi, Hideaki, ...
Abstract Background Panda ( s ) is an autosomal recessive mutation, which displays overall white plumage color with spots of wild-type plumage in the Japanese quail ( Coturnix japonica ). In a...
A new type system for deadlock-free processes (2006)
Abstract. We extend a previous type system for the π-calculus that guarantees deadlock-freedom. The previous type systems for deadlockfreedom either lacked a reasonable type inference algorithm or...
Resource usage analysis for the π-calculus (2006)
Naoki Kobayashi, Kohei Suenaga, Lucian Wischik
Abstract. We propose a type-based resource usage analysis for the πcalculus extended with resource creation/access primitives. The goal of the resource usage analysis is to statically check that a...
A new type system for deadlock-free processes (2006)
Abstract. We extend a previous type system for the π-calculus that guarantees deadlock-freedom. The previous type systems for deadlockfreedom either lacked a reasonable type inference algorithm or...
Resource usage analysis for the π-calculus (2006)
Naoki Kobayashi, Kohei Suenaga, Lucian Wischik
Abstract. We propose a type-based resource usage analysis for the πcalculus extended with resource creation/access primitives. The goal of the resource usage analysis is to statically check that a...
Kobayashi, Naoki, Saito, Kazuaki, Tatsuya, Ozawa, Moriyama, Osamu, Kitsunezaki, So, Yamazaki, Yoshihiro, ...
Partial order reduction for verification of spatial properties of pi-calculus processes (2005)
Reynald Affeldt, Naoki Kobayashi
Mechanical tools have recently been developed that enable computer-aided verification of spatial properties of concurrent systems. To be practical, these tools are expected to deal with the...
Kohei Suenaga, Naoki Kobayashi, Akinori Yonezawa
Abstract. In our previous paper, we have proposed a framework for automatically translating tree-processing programs into stream-processing programs. However, in writing programs that require...
Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes (2004)
Reynald Affeldt, Naoki Kobayashi
Mechanical tools have recently been developed that enable computer-aided verification of spatial properties of concurrent systems. To be practical, these tools are expected to deal with the...
A Coq Library for Verification of Concurrent Programs (2004)
Reynald Affeldt, Naoki Kobayashi
Thanks to recent advances, modern proof assistants now enable verification of realistic sequential programs. However, regarding the concurrency paradigm, previous work essentially focused on...
Type systems for concurrent programs (2003)
Abstract. Type systems for programming languages help reasoning about program behavior and early finding of bugs. Recent applications of type systems include analysis of various program behaviors...
Useless-Code Elimination and Program Slicing for the Pi-Calculus (2003)
In this paper, we study program transformations called uselesscode elimination and program slicing in the context of the #-calculus.
Time Regions and Effects for Resource Usage Analysis (2003)
Various resources such as files and memory are associated with certain protocols about how they should be accessed. For example, a memory cell that has been allocated should be eventually...
Useless-Code Elimination and Program Slicing for the Pi-Calculus (2003)
In this paper, we study program transformations called uselesscode elimination and program slicing in the context of the #-calculus.
Formalization and Verification of a Mail Server in Coq (2003)
Reynald Affeldt, Naoki Kobayashi
This paper reports on the formalization and verification of a mail server (SMTP server) in Coq. The correctness of a mail server is very important: bugs of the mail server may be abused for...
Type-Based Information Flow Analysis for the Pi-Calculus (2003)
We propose a new type system for information flow analysis for the
Time Regions and Effects for Resource Usage Analysis (2003)
Various resources such as files and memory are associated with certain protocols about how they should be accessed. For example, a memory cell that has been allocated should be eventually...
How Does Naked Singularity Look? (2002)
Nakao, Ken-ichi, Kobayashi, Naoki, Ishihara, Hideki
There are non-radial null geodesics emanating from the shell focusing singularity formed at the symmetric center in a spherically symmetric dust collapse. In this article, assuming the...
MPEG-4 very low bit-rate video compression by adaptively utilizing sprite to short sequences (2002)
Jinzenji, Kumi, Okada, Shigeki, Kobayashi, Naoki, Watanabe, Hiroshi
AnZenMail: A secure and certified e-mail system (2002)
Etsuya Shibayama, Shigeki Hagihara, Naoki Kobayashi, Shin-ya Nishizaki, Kenjiro Taura, Takuo Watanabe
Abstract. We are developing a secure and certified e-mail system AnZen-Mail that provides an experimental testbed for our cutting-edge security enhancement technologies. In addition to a provably...
A Type System for Lock-Free Processes (2002)
Interpretation. An alternative way to analyze the behavior of a concurrent program would be to use abstract interpretation [4, 5]. Actually, from a very general viewpoint, our type-based analysis of...
Type Systems for Concurrent Programs (2002)
Type systems for programming languages help reasoning about program behavior and early finding of bugs. Recent applications of type systems include analysis of various program behaviors such as side...
Type-Based Information Flow Analysis for Low-Level Languages (2002)
Naoki Kobayashi, Keita Shirane
A static program analysis called information flow analysis has been studied for high-level programming languages, to check that programs do not leak information about secret data such as passwords.
A generic type system for the Pi-calculus (2001)
Atsushi Igarashi, Naoki Kobayashi
We propose a general, powerful framework of type systems for the #-calculus, and show that we can obtain as its instances a variety of type systems guaranteeing non-trivial properties like...
A generic type system for the Pi-calculus (2001)
Atsushi Igarashi, Naoki Kobayashi
We propose a general, powerful framework of type systems for the π-calculus, and show that we can obtain as its instances a variety of type systems guaranteeing non-trivial properties like...
A generic type system for the Pi-calculus (2001)
Atsushi Igarashi, Naoki Kobayashi
We propose a general, powerful framework of type systems for the-calculus, and show that we can obtain as its instances a variety of type systems guaranteeing non-trivial properties like...
Type Reconstruction for Linear Pi-Calculus with I/O Subtyping (2001)
Atsushi Igarashi, Naoki Kobayashi
Powerful concurrency primitives in recent concurrent languages and thread libraries provide great flexibility about implementation of high-level features like concurrent objects.
Online-and-Offline Partial Evaluation: A Mixed Approach (Extended Abstract) (2000)
This paper presents a hybrid method of partial evaluation (PE), which combines the power of online PE and the efficiency of offline PE, for a typed strict functional language. We begin with a naive...
Type Reconstruction for Linear Pi-Calculus with I/O Subtyping (2000)
Atsushi Igarashi, Naoki Kobayashi
Powerful concurrency primitives in recent concurrent languages and thread libraries provide great exibility about implementation of high-level features like concurrent objects. However, they are so...
Online type-directed partial evaluation for dynamically-typed languages (2000)
This article presents an alternative method of type-directed partial evaluation, which is simpler and more efficient than previous methods. Unlike previous methods, it is straightforwardly applicable...
Online Type-Directed Partial Evaluation for Dynamically-Typed Languages (1999)
This article presents an alternative method of type-directed partial evaluation, which is simpler and more efficient than previous methods. Unlike previous methods, it is straightforwardly applicable...
Linear types (types of values that can be used just once) have been drawing a great deal of attention because they are useful for memory management, in-place update of data structures, etc.: an...
Linear types (types of values that can be used just once) have been drawing great attentions because they are useful for memory management, in-place update of data structures, etc.: an obvious...
A generalized deadlock-free process calculus (1998)
Naoki Kobayashi, Shin Saito, Eijiro Sumii
Abstract. We extend Kobayashi and Sumii’s type system for the deadlock-free π-calculus and develop a type reconstruction algorithm. Kobayashi and Sumii’s type system helps high-level reasoning...
A generalized deadlock-free process calculus (1998)
Naoki Kobayashi, Shin Saito, Eijiro Sumii
Abstract. We extend Kobayashi and Sumii's type system for the deadlockfree-calculus and develop a type reconstruction algorithm. Kobayashi and Sumii's type system helps high-level reasoning...
A partially deadlock-free typed process calculus (1998)
We propose a novel static type system for a process calculus, which ensures both partial deadlockfreedom and partial confluence. The key novel ideas are (1) introduction of the order of channel use...
Linearity and the Pi-Calculus (1998)
Naoki Kobayashi, Benjamin C. Pierce, David N. Turner, An Teallach Limited
The economy and flexibility of the pi-calculus make it an attractive object of theoretical study and a clean basis for concurrent language design and implementation. However, such generality has a...
Type-based Analysis of Communication for Concurrent Programming Languages (1997)
Atsushi Igarashi Naoki, Atsushi Igarashi, Naoki Kobayashi, Naoki Kobayashi
Powerful concurrency primitives in recent concurrent languages and thread libraries provide the great flexibility about implementation of high-level features like concurrent objects. However, they...
Type-based Analysis of Communication for Concurrent Programming Languages (1997)
Atsushi Igarashi, Naoki Kobayashi
. Powerful concurrency primitives in recent concurrent languages and thread libraries provide the great flexibility about implementation of high-level features like concurrent objects. However, they...
A Partially Deadlock-free Typed Process Calculus (II) (1997)
We propose a novel static type system for a process calculus, which ensures both partial deadlock-freedom and partial confluence. The key novel ideas are (1) introduction of order of channel use as...
Type-based Analysis of Communication for Concurrent Programming Languages (1997)
Atsushi Igarashi, Atsushi Igarashi, Naoki Kobayashi, Naoki Kobayashi
Powerful concurrency primitives in recent concurrent languages and thread libraries provide the great flexibility about implementation of high-level features like concurrent objects. However, they...
Partial Evaluation Scheme for Concurrent Languages and its Correctness (1996)
Haruo Hosoya Naoki, Naoki Kobayashi, Akinori Yonezawa
. A simple, general, and well-formalized partial evaluation method for concurrent languages is proposed. In spite of many potential benefits, there are few partial evaluation techniques for...
Linearity and the Pi-Calculus (1996)
Naoki Kobayashi, Benjamin C. Pierce, David N. Turner
The economy and flexibility of the pi-calculus make it attractive both as an object of theoretical study and as a basis for concurrent language design and implementation. However, such generality has...
A Partially Deadlock-free Typed Process Calculus (I) -- A Simple System -- (1996)
Concurrency primitives play an important role in describing programs on parallel /distributed environments and also in writing interactive programs. Theoretical supports for concurrency primitives,...
Higher-Order Concurrent Linear Logic Programming (1995)
Naoki Kobayashi, Akinori Yonezawa
. We propose a typed, higher-order, concurrent linear logic programming called higher-order ACL, which uniformly integrates a variety of mechanisms for concurrent computation based on asynchronous...
Static Analysis on Communication for Asynchronous Concurrent Programming Languages (1995)
Naoki Kobayashi, Naoki Kobayashi, Motoki Nakade, Motoki Nakade, Motoki Nakade, Akinori Yonezawa, ...
We propose an effect-based static analysis technique on communication for asynchronous concurrent programming languages. Our analysis gives an upper-bound of the number of enqueued messages and...
Static Analysis of Communication for Asynchronous Concurrent Programming Languages (1995)
Naoki Kobayashi Motoki, Naoki Kobayashi, Motoki Nakade, Akinori Yonezawa
. We propose an effect-based static analysis technique on communication for asynchronous concurrent programming languages. Our analysis gives an upper-bound of the number of enqueued messages and...
Linearity and the Pi-Calculus (1995)
Naoki Kobayashi, Benjamin C. Pierce, David N. Turner
A static type system with "use-once" channel types, inspired by linear logic, is applied to a pure calculus of processes and message passing. Applications of this type system include static...
Asynchronous Communication Model Based on Linear Logic (1995)
Naoki Kobayashi, Akinori Yonezawa
We propose a new framework called ACL for concurrent computation based on linear logic. ACL is a kind of linear logic programming framework, where its operational semantics is described in terms of...
Static Analysis on Communication for Asynchronous Concurrent Programming Languages (1995)
Naoki Kobayashi, Naoki Kobayashi, Motoki Nakade, Motoki Nakade, Motoki Nakade, Akinori Yonezawa, ...
We propose an effect-based static analysis technique on communication for asynchronous concurrent programming languages. Our analysis gives an upper-bound of the number of enqueued messages and...
Static Analysis of Communication for Asynchronous Concurrent Programming Languages (1995)
Naoki Kobayashi, Motoki Nakade, Akinori Yonezawa
. We propose an effect-based static analysis technique on communication for asynchronous concurrent programming languages. Our analysis gives an upper-bound of the number of enqueued messages and...
Typed Higher-Order Concurrent Linear Logic Programming (1994)
Naoki Kobayashi, Akinori Yonezawa
We propose a typed, higher-order, concurrent linear logic programming called higher-order ACL, which uniformly integrates a variety of mechanisms for concurrent computation based on asynchronous...
PARCS: An MPP-Oriented CLP Language (1994)
Kazuhiro Konno, Nagatsuka Masaaki, Naoki KOBAYASHI, Matsuoka Satoshi, Yonezawa Akinori
: PARCS is a declarative parallel constraint logic programming (CLP) language designed for efficient execution on distributed memory massively parallel processors (MPPs). As a language model, PARCS...
Reasoning on actions and change in a linear logic programming (1993)
Naoki Kobayashi, Akinori Yonezawa
Although traditional logic programming has been widely used in a world of artificial intelligence, it often lacks the ability to directly reason about dynamic change of knowledge. New logic...
ACL - A Concurrent Linear Logic Programming Paradigm (1993)
Naoki Kobayashi, Akinori Yonezawa
We propose a novel concurrent programming framework called ACL. ACL is a variant of linear logic programming, where computation is described in terms of bottom-up proof search of some formula in...
Logical, Testing, and Observation Equivalence for Processes in a Linear Logic Programming (1993)
Naoki Kobayashi, Akinori Yonezawa
Linear logic programming has recently been proposed and shown to be able to integrate a wide range of mechanisms for concurrent computation uniformly in terms of proof search. This paper introduces...
Control in Parallel Constraint Logic Programming (1991)
Naoki Kobayashi, Satoshi Matsuoka, Akinori Yonezawa
Although constraint satisfaction problems can be specified declaratively, the cost of actual solving depends heavily on the order of computation. The ideal combination of declarative problem...
Mapping of panda plumage color locus on the microsatellite linkage map of the Japanese quail
Miwa, Mitsuru, Inoue-Murayama, Miho, Kobayashi, Naoki, Kayang, Boniface Baboreka, Mizutani, Makoto, Takahashi, Hideaki, ...
Mapping of panda plumage color locus on the microsatellite linkage map of the Japanese quail
Miwa, Mitsuru, Inoue-Murayama, Miho, Kobayashi, Naoki, Kayang, Boniface Baboreka, Mizutani, Makoto, Takahashi, Hideaki, ...
Distributed Concurrent Linear Logic Programming
Naoki Kobayashi, Toshihiro Shimizu, Akinori Yonezawa
We propose a framework of distributed concurrent linear logic programming, which can elegantly capture the essential features of distributed computation: locationdependence /independence of names and...