Robin Milner. Functions as processes. Journal of Mathematical Structures in Computer Science, 2(2):119-141, 1992.  @ NUS  Home/Search   Document Not in Database   Summary   Related Articles   Check

....0 j 0, def D in new x P j new x def D in P if x 62 fn(D) def D in P ) j Q j def D in P j Q if fv(D) fv(Q) 5. x)P ) v] j P [ v= x] 6. l 1 = A1 ; l 2 = A2) j (l 2 = A2 ; l 1 = A1 ) X1 = A1 and X2 = A2) j (X2 = A2 and X1 = A1 ) Rules 1 and 2 are conventional in process calculi [12]. The novelty is the rules for def; rule 4 implements for def what rule 3 does for new (cf. 7] Rule 5 implements abstraction instantiation by replacing the formal parameters by the actuals. One could be tempted to introduce a rule for joining definitions def D in def D in P j def D and ....

.... ; Pn to a fl 1 = x 1 )P 1 ; l n = x n )P n g: Using axioms Inst and Com, and rule Str we can easily see that a l i [ v] j a fl 1 = A 1 ; l n = An g A i [ v] j a fl 1 = A 1 ; l n = An g; which constitutes the rule for replication in the calculus [12]. 3. Type assignment This section presents two type systems for the calculus of objects. The monomorphic type system TA Com a l i [ v] j a fl 1 = A 1 ; l n = An g A i [ v] 1 i n) Inst def D and X = A in X [ v] j P def D and X = A in A[ v] j P P j Q P j Q Res new x P ....

[Article contains additional citation context not shown here]

Robin Milner. Functions as processes. Journal of Mathematical Structures in Computer Science, 2(2):119--141, 1992.

.... lazy abstract machine, Curien proposed a di#erent environment machine, which we call CAM throughout this paper [4] From a di#erent community, two interpretations of the call by value # calculus into the # calculus are known: one proposed by Milner, and further studied by Pierce and Sangiorgi [7, 8, 9], the other proposed by the author, but lacking, to date, a systematic study [13] In his paper on encodings of the # calculus into the # calculus, Milner uses the term environment entry to describe a process simulating the behaviour of some function on a given channel [7, 8] The term comes ....

.... and Sangiorgi [7, 8, 9] the other proposed by the author, but lacking, to date, a systematic study [13] In his paper on encodings of the # calculus into the # calculus, Milner uses the term environment entry to describe a process simulating the behaviour of some function on a given channel [7, 8]. The term comes probably from the so called environment machines, devices that describe implementations of the # calculus, capable of e#ciently performing substitutions by maintaining a map from variables to function closures (the environment) The natural question arises as what is the relation ....

[Article contains additional citation context not shown here]

Robin Milner. Functions as processes. Journal of Mathematical Structures in Computer Science, 2(2):119--141, 1992.

....it treats constraint handling logically . In contrast to [8, 14] our semantics accounts for order (of goals and alternatives) cut and eager wakening and ignores declarative semantics. Our approach is based on abstract tree rewriting which appeared in a revised representation of the calculus [9] and was employed in [15, 16] to formulate calculi for higher order concurrent constraint programming model. The abstract tree rewriting model proves particularly useful for constraint programming since constraint propagation and simplification (for testing satisfiability as well as entailment) ....

R. Milner. Functions as Processes. In Journal of Mathematical Structures in Computer Science 2:2, pages 119--141, 1992.

....contrast to the recently proposed call by need calculus, our concurrent call by need model incorporates mutual recursion and can be extended to cyclic data structures by means of constraints. 1 Introduction We investigate concurrency as unifying computational paradigm in the spirit of Milner [Mil92] and Smolka [Smo94, Smo95b] Whereas the motivations for both approaches are quite distinct, the resulting formalisms are closely related: The calculus [MPW92] models communication and synchronisation via channels, whereas the ae calculus [NS94, Smo94, NM95] uses logic variables or more ....

....whereas the ae calculus [NS94, Smo94, NM95] uses logic variables or more generally constraints as inspired by [Mah87, SRP91] Our motivation in concurrent calculi lies in the design of programming languages. Concurrency enables us to integrate multiple programming paradigms such as functional [Mil92, Smo94, Nie94, Iba95, PT95b], object oriented [Vas94, PT95a, HSW95, Wal95] and constraint programming [JH91, SSW94] All these paradigms are supported by the programming language Oz [Smo95a, Smo95b] In this paper, we model the time complexity of eager and lazy functional computation in a concurrent calculus. The ....

[Article contains additional citation context not shown here]

Robin Milner. Functions as processes. Journal of Mathematical Structures in Computer Science, 2(2):119--141, 1992.

.... Call by Name to Call by Need 28 16 Relating Call by Value to Call by Need 39 17 Adequacy of the Embedding of ffi into ffi 0 41 18 Simulating the Call by Need Calculus 45 19 Conclusion 46 1 Introduction We investigate concurrency as unifying computational paradigm in the spirit of Milner [Mil92] and Smolka [Smo94, Smo95b] Whereas the motivations for both approaches are quite distinct, the resulting formalisms are closely related: The calculus [MPW92] models communication and synchronisation via channels, whereas the ae calculus [NS94, Smo94, NM95] uses logic variables or more ....

....whereas the ae calculus [NS94, Smo94, NM95] uses logic variables or more generally constraints as inspired by [Mah87, SRP91] Our motivation in concurrent calculi lies in the design of programming languages. Concurrency enables us to integrate multiple programming paradigms such as functional [Mil92, Smo94, Nie94, Iba95, PT95b], object oriented [Vas94, PT95a, HSW95, Wal95] and constraint programming [JH91, SSW94] All these paradigms are supported by the programming language Oz [Smo95a, Smo95b] In this paper, we model the time complexity of eager and lazy functional computation in a concurrent calculus. The ....

[Article contains additional citation context not shown here]

Robin Milner. Functions as processes. Journal of Mathematical Structures in Computer Science, 2(2):119--141, 1992.

....from Hewitt s actor model of computation [6] However, both models have in common that they are inherently concurrent (Hewitt speaks of ultra concurrency) a class of expressions modulo a structural congruence. This set up, which is also employed in more recent presentations of the calculus [8, 7], proves particularly useful for Oz since constraint propagation and simplification can be accommodated elegantly by means of the structural congruence. Kernel Oz itself consists of a class of expressions whose semantics is defined by a translation into the elaborable expressions of the actor ....

....model can be seen as a computational metaphor for the calculus providing motivation and intuition. The Oz calculus models concurrent computation as rewriting of a class of expressions modulo a structural congruence. This set up, which is also employed in more recent presentations of the calculus [8, 7], proves particularly useful for Oz since constraint propagation and simplification can be accommodated elegantly by means of the structural congruence. The Oz calculus is not committed to a particular constraint system; instead, it is parameterized with respect to a general and straightforward ....

Robin Milner. Functions as processes. Journal of Mathematical Structures in Computer Science, 2(2):119--141, 1992.

....basic issues of higher order process calculi, including their expressivity. We regard reduction strategies as an important but orthogonal issue. Reduction strategies are best understood separately, on the calculus. Encodings of various calculus reduction strategies into calculus are studied in [25, 37]. Xi Barbed congruence is dened in LHO as by Denition 3.2 (take the calculus L in the denition to be LHO) Remark 4.7 The language of LHO without replication is enough to write processes with an innite behaviour, for the same reason why the paradoxical operator Y can be written in the calculus. ....

R. Milner. Functions as processes. Journal of Mathematical Structures in Computer Science, 2(2):11914.

....to be communicated; jxyjP denotes jxj(jyj(P ) Finally we will freely use parenthesis to be explicit about syntactic construction. Reduction relation provides the basic notion of computing in the formalism. To formulate reduction we first stipulate a set of structural rules following Milner [14] (cf. 4] We define j to be the smallest equivalence relation over terms generated by: 1) P; Q) R j P; Q; R) 4) P; Q j Q; P (2) P; 3 j P (5) ax:P j ax(P; ax:P ) 3) jxjP; Q j jxj(P; Q) x 62 FN (Q) 6) P j Q then P; R j Q; R and jxjP j jxjQ. Let ; range over a sequence ....

....we refine the induced equations by considering exact steps a term needs to reach another semantic point. 3 Discussion 3. 1. Reduction theories for other Calculi. This section briefly summarized that results for applying our construction to not only other process calculi (CCS[11, 13] calculus[12, 14]) but also calculus. CCS. One essential issue in constructing reduction theories for CCS is that the summation is problematic in weak congruent theories in general. However we restore weak bisimilarity in our purely equational setting by considering the maximum sound theory among subset of ....

[Article contains additional citation context not shown here]

Milner, R., Functions as Processes. In Automata, Language and Programming, LNCS 443, 1990.

....first at a, then at b, then at a again. Further, the number of redexes increases exponentially in its course, but the computation terminates. Such behaviour occurs when a process requests the same resource more than once in an interaction, e.g. in an encoding of the l term lxyz: xz) yz) [49]. The difficulty in analysing (4) can be seen by considering the following subterm of a one step descendant of (4) nc) c j c j Fwhcbi) It contains a chain c b, which is difficult to determine before c is passed. But if we naively represent causality incorporating bound names in (4) there is ....

....strong bisimilarity (which does not change termination) together with replication theorems [11, 51, 57] Finally acyclicity in causality yields strong normalisation. Summary of Contributions. The following summaries main technical contributions of the present paper. 4) solves an open problem in [49] for the simple type hierarchy. 1) Introduction of a linear p calculus in which where strong normalisability is ensured by typability. 2) Establishment of the proof methodology for strong normalisability of typable processes, combining ideas from traditional SN proofs for typed l calculi with ....

[Article contains additional citation context not shown here]

Milner, R., Functions as Processes. MSCS, 2(2), 119--146, CUP, 1992.

....first at a, then at b, then at a again. Further, the number of redexes increases exponentially in its course, but the computation terminates. Such behaviour occurs when a process requests the same resource more than once in an interaction, e.g. in an encoding of the l term lxyz: xz) yz) [33]. The difficulty in analysing (1) can be seen by considering the following subterm of a one step descendant of (1) nc) chv 1 i j chv 2 i j Fwhcbi) It contains a chain c b, which is difficult to determine before c is passed. In fact, if we naively represent causality incorporating bound ....

....by strong bisimilarity (which does not change termination) together with replication theorems [9, 35, 41] Then acyclicity in causality yields strong normalisation. Summary of Contributions The following summarises main technical contributions of the present work. 3) solves an open problem in [33] for the simple type hierarchy. 1. Introduction of a typed p calculus where strong normalisability is ensured by typability. SN has significant consequences for the calculus, including the finite axiomatisation of the weak bisimilarity and the basic liveness in interaction. 2. Establishment of ....

[Article contains additional citation context not shown here]

Milner, R., Functions as Processes. MSCS, 2(2), 119--146, CUP, 1992.

....functional computation. The precision of the representation is demonstrated by way of a fully abstract encoding of PCF. Preceding studies have shown that while operational encodings of diverse programming language constructs into the calculus are possible, they are rarely fully abstract [30, 35]: we necessarily lose information by such a translation. This is because the translation of a source term M will generally result in a process containing more behaviour than M . Type disciplines for the calculus with signi cant properties such as linearity and deadlock freedom have been studied ....

....evaluation. From a di erent viewpoint, our work shows an e ective way to apply game semantics to the study of basic typing systems for the calculus, in particular for the proof of full abstraction of encodings. Concerning the use of the calculus as the target language for translations, [30] was the rst to point out the diculty of fully abstract embeddings of functional sequentiality in the calculus and [35] showed that the same problems arise even with the higher order calculus. While some preceding work studies the signi cance of replication and linearity of channels [9, 17, ....

[Article contains additional citation context not shown here]

Milner, R., Functions as Processes. MSCS, 2(2), 119-146, CUP, 1992.

....and to (ii) define an unified paradigm which fulfills our requirements. Common to both approaches mentioned above is the fact that all language features are defined by transformation to a core language that implements the #L calculus [Lum99] an inherently polymorphic variant of the # calculus [Mil90, HT91] in which agents communicate by passing forms (a special notion of extensible records) rather than tuples. By this approach, we address the problem that reusability and extensibility of software components is limited due to position dependent parameters. Besides forms, which have their ....

....essential if we are to deal with multiple architectural styles and component models within a common, unifying framework. The simplest foundation that seems appropriate is that of communicating, concurrent agents. For this reason we have extensively explored the asynchronous polyadic # calculus [Mil90, HT91] as a tool for modelling objects, components, and software composition [LSN96, SL97] The tuple based communication of the # calculus, however, turns out to restrict extensibility and reuse. These observations have led us to explore communication of forms a special notion of extensible ....

[Article contains additional citation context not shown here]

Robin Milner. Functions as Processes. In Proceedings ICALP '90, LNCS 443, pages 167--180. Springer, July 1990.

....should have type N L due to non termination) Then we can observe that the high level channel x a ects an action at a low level channel u. The anomaly takes place because stateful agents can transmit information using time di erence, storing what has happened in its state to transmit it later [42]. Structurally secure types prevent this leakage by requiring that a stateful replication to transmit information at the same, or higher, level than it receives. Hereafter we assume all channel types are structurally secure. 6.4 Secrecy Typing with State The secrecy typing for stateful processes ....

Milner, R., Functions as Processes, MSCS. 2(2):119-141, 1992,

....this reason, attempts by Kleene [18 21] in his work on higher type recursion theory, and by Berry and Curien [9] in their work on sequential algorithms, failed to yield a characterization. Similarly, while there were encodings of the calculus into various process calculi such as the calculus [27], there was no characterization of which processes arose from these encodings. The more refined tools provided by game semantics led to a solution of this characterization problem, first in the case of the multiplicative fragment of linear logic [5] and then for PCF [1, 16, 29] Subsequently the ....

R. Milner. Functions as processes. In Proceedings of ICALP 90, volume 443 of Lecture Notes in Computer Science, pages 167--180. Springer-Verlag, 1990.

....The operational semantics of the calculi provides a precise and clear understanding of the algorithms behaviour, aiding design, and ultimately, one may hope, supporting proofs of correctness and robustness. Our presentation draws on ideas rst developed in Milner, Parrow, and Walker s calculus [MPW92,Mil92] and extended in the distributed join calculus of Fournet et al. [FGL 96] To facilitate experimentation, the Nomadic Pict project is implementing prototype mobile agent programming languages corresponding to our highand low level process calculi. The low level language extends the compiler and ....

....names. The informal descriptions of the primitives in x2 can be made precise by giving them an operational semantics. We adopt a reduction semantics, de ning the atomic state changes that a system of agents can undergo by reduction axioms with a structural congruence, following the style of [BB92,Mil92]. The process terms of the calculi in x2.1,2.2 only allow the source code of the body of a single agent to be expressed. During computation, this agent may evolve into a system of many agents, distributed over many sites. The reduction relation must be between the possible states of these ....

Robin Milner. Functions as processes. Journal of Mathematical Structures in Computer Science, 2(2):119-141, 1992.

....port of process and a communication partner by communication is possible. There are researches which use w calculus for semantics description and specification adapting the above features. Exampies are the expressing semantics of an object oriented lan guage [7] and the encodings of A calculus[4] and a programming language[1] based on r calculus. It is possible to use the above existing results and to describe a system and software by r calculus. However, these researches need to describe a behavior by combining functions of r calculus intricately. Since the description of a system ....

Milner, R.: Functions as processes, Journal of Mathematical Structure in Computer Science 2(2), pp.119141 (19).

....at higher types. Given this success, it is important to see how broad the scope of the approach initiated in [1, 4] actually is. In this paper, we consider the lazy calculus [2, 6] This calculus, and certain associated notions such as applicative simulation, have been quite widely influential [8, 11, 13, 14, 17, 19, 22]. In [6] a syntactic construction of a fully abstract model for the basic sequential language was given, and the canonical denotational model was shown to be fully abstract for a certain parallel extension of the language. However, the problem of giving a direct, syntax free, purely semantic ....

R. Milner. Functions as processes. In Proceedings of ICALP 90, volume 443 of Lecture Notes in Computer Science, pages 167--180. Springer-Verlag, 1990.

....work has been done on the compilation of whole languages into process calculi, exploring both semantics and expressiveness. Examples include translations between the process calculi CSP and CCS [Li83, Mil87] between the join calculus and the # calculus [FG96] of # calculi into process calculi [Mil92, San94b, Lav93, San94a, Tho95, San94b, San95a, ALT95, Ode95b, Nie96], data types and other sequential programming constructs [Mil89, Mil93, Wal91b, Ode95a] from object oriented languages into process calculi [Vaa90, Wal91a, Wal95, Wal93, Jon93, Wal94, PT95] from logic programming languages into the # calculus [Ros93, Li94] and from concurrent constraint ....

R. Milner. Functions as Processes. Journal of Mathematical Structures in Computer Science, 2(2):119--141,

....There is an evident notion of ff conversion P j ff Q, and renaming is written P [fi=ff] Terms are assigned to sequent proofs in CLL 2 as in Figure 2. Dynamics We now describe the dynamics of terms, corresponding to cut elimination of proofs. We factor this into two parts, in the style of [Mil90, Abr93]: a structural congruence j and a reduction relation . 28 Identity Group Multiplicative Units U ff ff : I ff ff : Gamma fl (P ) Gamma; fl : AEB Additive Unit ff;ff ff : Gamma; ff : P Gamma; ff : B (P; Q) Gamma; fl : A B P Gamma; ff : A; fi : A P ....

R. Milner. Functions as processes. In Proceedings of ICALP 90, volume 443 of Lecture Notes in Computer Science, pages 167--180. Springer-Verlag, 1990.

....a shows how we can get infinite behaviour through the use of self variables. The object a shows how an object can modify itself by performing a method override on a self variable. 3 The asynchronous calculus The calculus [PW92] has previously shown its ability to encode both the calculus [Mil92] and certain object oriented languages [Wal95, San96] In [Wal95] Walker encoded a variant of the programming language POOL [Ame89] into the calculus and in [San96] Sangiorgi investigates another encoding of the calculus into the calculus. Sangiorgi shows how to encode the calculus in a ....

Robin Milner. Functions as processes. Journal of Mathematical Structures in Computer Science, 2(2):119--141, 1992.

....of data arises naturally in the calculus. Another topic which we can hope to understand better through naming is object oriented programming; one of the cornerstones of this topic (which is still treated mostly informally) is the way in which objects provide access to one another by naming. In [17] I used the term object paradigm to describe models such as the calculus in which agents (objects) are assumed to persist and retain independent identity. David Walker [28] has had initial success in giving formal semantics to simple object oriented languages in the calculus. A challenging ....

....order initially, since the goal was to demonstrate that in some sense it is sufficiently powerful to allow only names or channels to be the content of communications. Indeed Thomsen s work supports this conjecture, and the present work strengthens his results comparing the approaches. See Milner [17] for a discussion contrasting the approaches. Outline There are six short chapters following this introduction. Chapter 2 reviews the formalism of the monadic calculus, essentially as it was presented in [19] it also defines the notion of structural congruence and the reduction relation as ....

[Article contains additional citation context not shown here]

Milner, R., Functions as processes, Research Report No. 1154, INRIA, Sophia Antipolis, February 1990. To appear in Journal of Mathematical Structures in Computer Science.

No context found.

Robin Milner. Functions as processes. Journal of Mathematical Structures in Computer Science, 2(2):119-141, 1992.

No context found.

Robin Milner. Functions as processes. Journal of Mathematical Structures in Computer Science, 2(2):119--141, 1992.

No context found.

Robin Milner. Functions as processes. Journal of Mathematical Structures in Computer Science, 2(2):119--141, 1992.

No context found.

R. Milner. Functions as processes. In Proceedings of ICALP 90, volume 443 of Lecture Notes in Computer Science, pages 167--180. Springer-Verlag, 1990.

No context found.

R. Milner. Functions as processes. In Proceedings of ICALP 90, volume 443 of Lecture Notes in Computer Science, pages 167--180. Springer-Verlag, 1990.

No context found.

Milner, R. (1992). Functions as processes. Mathematical Structures in Computer Science 2, 119-141.

No context found.

Robin Milner. Functions as processes. MSCS, 2(2):119--141, 1992.

No context found.

Milner, R., Functions as Processes. MSCS, 2(2), 119-146, CUP, 1992.

No context found.

R. Milner. Functions as processes. Journal of Mathematical Structures in Computer Science, 2(2):119--141, 1992.

No context found.

Milner, R., Functions as Processes. MSCS, 2(2), 119-146, CUP, 1992.

No context found.

Milner, R., Functions as Processes. MSCS, 2(2), 119-146, CUP, 1992.

No context found.

Milner, R., Functions as Processes, MSCS. 2(2):119--141, 1992,

No context found.

Milner, R., Functions as Processes, MSCS. 2(2):119-141, 1992,

No context found.

R. Milner "Functions as Processes", LNCS 443, 1990.

No context found.

R. Milner "Functions as Processes", LNCS 443, 1990.

No context found.

Milner, R. Functions as processes. MSCS 2, 2 (1992), 119-141.

No context found.

Milner, R., Functions as Processes, MSCS. 2(2):119-141, 1992,

No context found.

Milner, R., Functions as Processes. MSCS, 2(2), 119-146, CUP, 1992.

No context found.

Robin Milner. Functions as processes. MSCS, 2(2):119-141, 1992.

No context found.

Robin Milner. Functions as processes. Journal of Mathematical Structures in Computer Science 2(2), pages 119--141, 1992.

No context found.

Milner, R., Functions as Processes, MSCS. 2(2):119--141, 1992,

No context found.

R. Milner. Functions as processes. Journal of Mathematical Structures in Computer Science, 2(2):119-- 141, 1992.

No context found.

Milner, R., Functions as Processes, MSCS. 2(2):119-141, 1992,

No context found.

Milner, R., Functions as Processes, MSCS. 2(2):119--141, 1992,

No context found.

Robin Milner. Functions as processes. MSCS, 2(2):119-141, 1992.

No context found.

R. Milner, "Functions as Processes", LNCS 443, 1990.

No context found.

Milner, R., Functions as Processes. MSCS, 2(2), 119-146, CUP, 1992.

No context found.

R. Milner. Functions as processes. Math. Struc. in Computer Sciences, 2(2):119-- 141, 1992.

No context found.

Milner, R. (1992) Functions as processes. Math. Structures Compt. Sci. 2(2), 119{ 141.

First 50 documents  Next 50

Online articles have much greater impact   More about CiteSeer.IST at NUS   Add search form to your site   Submit documents   Feedback  

CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.