Publications
373 results found
Honda K, Yoshida N, 1999, Game-theoretic analysis of call-by-value computation, 24th International Colloquium on Algorithm, Languages and Programming (ICALP 97), Publisher: ELSEVIER SCIENCE BV, Pages: 393-456, ISSN: 0304-3975
- Author Web Link
- Cite
- Citations: 52
Yoshida N, Hennessy M, 1999, Subtyping and locality in distributed higher order processes, Pages: 557-572, ISSN: 0302-9743
This paper studies one important aspect of distributed systems, locality, using a calculus of distributed higher-order processes in which not only basic values or channels, but also parameterised processes are transferred across distinct locations. An integration of the sub typing of l-calculus and IO-sub typing of the p-calculus offers a tractable tool to control the locality of channel names in the presence of distributed higher order processes. Using a local restriction on channel capabilities together with a sub typing relation, locality is preserved during reductions even if we allow new receptors to be dynamically created by instantiation of arbitrary higher-order values and processes. We also show that our method is applicable to more general constraints, based on local and global channel capabilities. © Springer-Verlag Berlin Heidelberg 1999.
Yoshida N, Hennessy M, 1999, Subtyping and locality in distributed higher order processes - Extended abstract, 10th International Conference on Concurrency Theory (CONCUR 99), Publisher: SPRINGER-VERLAG BERLIN, Pages: 557-572, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 20
Yoshida N, 1998, Minimality and separation results on asynchronous mobile processes - Representability theorems by concurrent combinators (Extended abstract), 9th International Conference on Concurrency Theory (CONCUR 98), Publisher: SPRINGER-VERLAG BERLIN, Pages: 131-146, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 5
Honda K, Yoshida N, 1997, Game theoretic analysis of call-by-value computation, Pages: 226-236, ISSN: 0302-9743
We present a general semantic universe of call-by-value computation based on elements of game semantics, and vah'date its appropriateness as a semantic universe by the full abstraction result for call-by-value PCF, a generic typed programming language with call-by-value evaluation. The key idea is to consider the distinction between call-by-name and call-by-value as that of the structure of information flow, which determines the basic form of games. In this way call-by-name computation and call-by-value computation arise as two independent instances of sequential functional computation with distinct algebraic structures. We elucidate the type structures of the universe following the standard categorical framework developed in the context of domain theory. Mutual relationship between the presented category of games and the corresponding call-by-name universe is also clarified.
Honda K, Yoshida N, 1997, Game theoretic analysis of call-by-value computation, 24th International Colloquium on Algorithm, Languages and Programming (ICALP 97), Publisher: SPRINGER-VERLAG BERLIN, Pages: 225-236, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 13
Yoshida N, 1996, Graph types for monadic mobile processes, Pages: 371-386, ISSN: 0302-9743
While types for name passing calculi have been studied extensively in the context of sorting of polyadic π-calculus [5, 34, 9, 28, 32, 19, 33, 10, 17], the same type abstraction is not possible in the monadic setting, which was left as an open issue by Milner [21]. We solve this problem with an extension of sorting which captures dynamic aspects of process behaviour in a simple way. Equationally this results in the full abstraction of the standard encoding of polyadic π-calculus into the monadic one: the sorted polyadic π-terms are equated by a basic behavioural equality in the polyadic calculus if and only if their encodings are equated in a basic behavioural equality in the typed monadic calculus. This is the first result of this kind we know of in the context of the encoding of polyadic name passing, which is a typical example of translation of high-level communication structures into π-calculus. The construction is general enough to be extendable to encodings of calculi with more complex operational structures.
HONDA K, YOSHIDA N, 1995, ON REDUCTION-BASED PROCESS SEMANTICS, THEORETICAL COMPUTER SCIENCE, Vol: 151, Pages: 437-486, ISSN: 0304-3975
- Author Web Link
- Cite
- Citations: 166
Yoshida N, 1995, Graph notation for concurrent combinators, Pages: 393-412, ISSN: 0302-9743
We introduce graph notation for concurrent processes which does not use the notion of port names for its formulation. The operators in the algebra of graphs proposed in this paper are quite different from those in the original term representation, making such notions as connection and correspondence of communication ports explicit. We show how basic elements of process calculi such as agents, reduction, and behavioural equivalences are soundly formulated in the new setting. The work is based on the authors’ study on concurrent combinators [9, 10], and can be considered as offering another mathematical representation of the formal notion studied therein.
Honda K, Yoshida N, 1994, Replication in concurrent combinators, Pages: 786-805, ISSN: 0302-9743
We establish the behavioural representability of input prefix and replication, which are two basic operators of the asynchronous ν-calculus [5, 6] (cf. [2]), an offspring of π-calculus [14, 11], in a system of concurrent combinators which is an extension of cc [7]. Systems of concurrent combinators axe simple formal systems based on a finite number of atoms with fixed interaction rules and two connectives for term formation, namely, concurrent composition and name hiding. Since such a system does not own inductively defined syntactic constructs for prefix or replication, their representability using a fixed number of atoms is theoretically interesting, reminiscent of the similar results obtained by Schönfinkel and Curry in the context of the classical combinators.
Honda K, Yoshida N, 1994, Combinatory representation of mobile processes, Pages: 348-360, ISSN: 0730-8566
A theory of combinators in the setting of concurrent processes is formulated. The new combinators are derived from an analysis of the operation called asynchronous name passing, just as an analysis of logical substitution gave rise to the sequential combinators. A system with seven atoms and fixed interaction rules, but with no notion of prefixing, is introduced, and is shown to be capable of representing input and output prefixes over arbitrary terms in a behaviorally correct way, just as SK-combinators are closed under functional abstraction without having it as a proper syntactic construct. The basic equational correspondence between concurrent combinators and a system of asynchronous mobile processes, as well as the embedding of the finite part of π-calculus in concurrent combinators, is proved. These results will hopefully serve as a cornerstone for further investigation of the theoretical as well as pragmatic possibilities of the presented construction.
Yoshida N, 1993, Optimal reduction in weak-λ-calculus with shared environments, Pages: 243-251
We introduce a weak-λ-calculus called λf-calculus which formalizes functional execution with shared environments in a clean and tractable way. It effectively incorporates the notion of name passing into the functional regime, treating variables in environments as channels of communication. This enables simple formulation of reduction rules under a sequence of shared environments, resulting in a functional calculus whose weak reduction enjoys several pleasant syntactic properties, e.g. the Church-Rosser property and normalizability. We also show that the leftmost reduction strategy of the calculus is optimal in the weak execution scheme.
Honda K, Yoshida N, 1993, On reduction-based process semantics, Pages: 373-387, ISSN: 0302-9743
A formulation of semantic theories for processes which is based on reduction relation and equational reasoning is studied. The new construction can induce meaningful theories for processes, both in stroug and weak settings. The resulting theories in many cases coincide with, and sometimes generallse, observation-based formulation of behavioural equivalence. The basic construction of reduction-based theories is studied, taking a simple name passing calculus called v-calculus as an example. Results on other calculi are also briefly discussed.
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.