Loading...
Please wait, while we are loading the content...
Similar Documents
On Typing Systems for the Polyadic $\pi$-Calculus(Concurrency Theory and Applications '96)
| Content Provider | Semantic Scholar |
|---|---|
| Author | Togashi, Atsushi |
| Copyright Year | 1997 |
| Abstract | In the literature, there have been intensive studies on typing (sorting) systems for the polyadic $\pi$-calculus, originated by Milner’s sorting discipline [10] based on name matching. The proposed systems, so far, are categorized into the two groups –systems by name matching and ones by structure matching (possibly with sub$\mathrm{t}\mathrm{y}\mathrm{p}\mathrm{i}\mathrm{n}\mathrm{g})-\mathrm{a}\mathrm{n}\mathrm{d}$ obtain similar results. A natural question arises “Is there any relationship between the two paradigms ?”. With this motivation, the present paper gives per investigations on typing systems between the two approaches. For this purpose, a sorting system by name matching, a quite similar to the system in [7], and a typing system by structure matching with subtyping, a slight extension of the system in [12], are presented, along with several basic properties. Then, correspondence between the sorting system and the typing system is investigated via transformations both form sortings to typings and from typings to sortings. It is shown that if a process is $\mathrm{w}\mathrm{e}\mathrm{l}1_{-}\mathrm{s}\mathrm{o}\mathrm{r}\mathrm{t}\mathrm{e}\mathrm{d}w.r.i$. a safe sorting in the sorting system, then it is well-typed for the transformed typing in the typing system, but not vice versa. This result can be straightforwardly extended to Liu and Walker’s consistent sortings. Under a certain condition, we can show the reverse implication. Furtheremore, on the other direction from typings to sortings, it is shown that the derived typing from the sorting which is the result of applying transformation to a typing coincides with the original typing. However, the derived sorting from the typing which is the result of applying transformation to a sorting is proved to be a proper specialization of the original sorting. *The work has been done during visiting the COGS, University of Sussex, Farmer, Brighton BN1 $9\mathrm{Q}\mathrm{H}$ , England. 数理解析研究所講究録 996巻 1997年 125-142 125 |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | https://repository.kulib.kyoto-u.ac.jp/dspace/bitstream/2433/61234/1/0996-12.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
