article

Open access

A partially deadlock-free typed process calculus

Editor: William Pugh Author:

Naoki KobayashiAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 20, Issue 2

Pages 436 - 482

https://doi.org/10.1145/276393.278524

Published: 01 March 1998 Publication History

PDF eReader

References

[1]

BERGER, M., GAY, S., AND NAGARAJAN, R. 1997. A typed calculus of deadlock-free processes. Draft paper, Imperial College, London.

Google Scholar

[2]

COLBY, C. 1995. Analyzing the communication topology of concurrent programs. In Proceedings of the A CM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation. ACM Press, New York, 202-213.

Crossref

Google Scholar

[3]

GAY, S. J. 1993. A sort inference algorithm for the polyadic 7r-calculus. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, 429-438.

Crossref

Google Scholar

[4]

HODAS, J. S. AND MILLER, D. 1994. Logic programming in a fragment of intuitionistic linear logic. Inf. Comput. 110, 2, 327-365.

Crossref

Google Scholar

[5]

HONDA, K. AND YOSHIDA, N. 1995. On reduction-based process semantics. Theor. Comput. Sci. 151, 2, 437-486.

Crossref

Google Scholar

[6]

IGARASHI, A. AND KOBAYASHI, N. 1997. Type-based analysis of usage of communication channels for concurrent programming languages. In Proceedings of International Static Analysis Symposium (SAS'97). Lecture Notes in Computer Science, vol. 1302. Springer-Verlag, Berlin, 187-201.

Crossref

Google Scholar

[7]

KOBAYASHI, N. 1996a. Concurrent linear logic programming. Ph.D. thesis, Dept. of Information Science, Univ. of Tokyo, Japan.

Google Scholar

[8]

KOBAYASHI, N. 1996b. A partially deadlock-free typed process calculus (I)--a simple system. Tech. Rep. 96-02, Dept. of Information Science, Univ. of Tokyo, Japan.

Google Scholar

[9]

KOBAYASHI, N. AND YONEZAWA, A. 1995. Towards foundations for concurrent object-oriented programming--types and language design. Theory Pract. Object Syst. 1, 4, 243-268.

Crossref

Google Scholar

[10]

KOBAYASHI, N., PIERCE, B. C., AND TURNER, D. N. 1996. Linearity and the pi-calculus. In Proceedings of A CM SIGPLAN/SIGA CT Symposium on Principles of Programming Languages. ACM Press, New York, 358-371.

Crossref

Google Scholar

[11]

MACKIE, I. 1994. Lilac: A functional programming language based on linear logic. J. Funct. Program. 4, 4 (Oct.), 1-39.

Google Scholar

[12]

MILNER, R. 1990. Function as processes. In Automata, Language and Programming. Lecture Notes in Computer Science, vol. 443. Springer-Verlag, Berlin, 167-180.

Crossref

Google Scholar

[13]

MILNER, R. 1993. The polyadic 7r-calculus: A tutorial. In Logic and Algebra of Specification, F. L. Bauer, W. Brauer, and H. Schwichtenberg, Eds. Springer-Verlag, Berlin.

Google Scholar

[14]

MILNER, R., PARROW, J., AND WALKER, D. 1992. A calculus of mobile processes, I, II. Inf. Comput. 100, 1-77.

Crossref

Google Scholar

[15]

NESTMANN, U. 1997. What is a 'good' encoding of guarded choice? In Proceedings of EXPRESS'97. Electronic Notes in Theoretical Computer Science, vol. 7. Elsevier Science Publishers, Amsterdam.

Google Scholar

[16]

NIELSON, H. R. AND NIELSON, F. 1994. Higher-order concurrent programs with finite communication topology. In Proceedings of A CM SIGPLAN/SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, 84-97.

Crossref

Google Scholar

[17]

OSTHEIMER, G. AND DAVIE, A. J. T. 1993. 7r-calculus characterizations of some practical A-calculus reduction strategies. Tech. rep., St. Andrews Univ., Scotland.

Google Scholar

[18]

OYAMA, Y., TAURA, K., AND YONEZAWA, A. 1997. An efficient compilation framework for languages based on a concurrent process calculus. In Proceedings of Euro-Par '97 Parallel Processing, Object-Oriented Programming. Lecture Notes in Computer Science, vol. 1300. Springer-Verlag, Berlin, 546-553.

Crossref

Google Scholar

[19]

PEYTON JONES, S. 1996. Concurrent Haskell. In Proceedings of A CM SIGPLAN/SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, 295-308.

Crossref

Google Scholar

[20]

PIERCE, B. AND SANGIORGI, D. 1993. Typing and subtyping for mobile processes. In Proceedings of IEEE Symposium on Logic in Computer Science. IEEE, New York, 376-385.

Google Scholar

[21]

PIERCE, B. C. AND SANGIORGI, D. 1997. Behavioral equivalence in the polymorphic pi-calculus. In Proceedings of A CM SIGPLAN/SIGA CT Symposium on Principles of Programming Languages. ACM Press, New York, 242-255.

Crossref

Google Scholar

[22]

PIERCE, B. C. AND TURNER, D. N. 1995. Concurrent objects in a process calculus. In Theory and Practice of Parallel Programming (TPPP). Lecture Notes in Computer Science, vol. 907. Springer-Verlag, Berlin, 187-215.

Crossref

Google Scholar

[23]

PIERCE, B. C. AND TURNER, D. N. 1997. Pict: A programming language based on the pi-calculus. Tech. rep., Computer Science Dept., Indiana Univ. To appear in Milner Festschrift, MIT Press, 1997.

Google Scholar

[24]

REPPY, J. H. 1991. CML: A higher-order concurrent language. In Proceedings of the ACM SIGPLAN'91 Conference on Programming Language Design and Implementation. ACM Press, New York, 293-305.

Crossref

Google Scholar

[25]

SANGIORGI, D. 1992. Expressing mobility in process algebras: First-order and higher-order paradigms. Ph.D. thesis, Univ. of Edinburgh, Edinburgh, Scotland.

Google Scholar

[26]

SANGIORGI, D. 1997. The name discipline of uniform receptiveness (extended abstract). In Proceedings of ICALP'97. Lecture Notes in Computer Science, vol. 1256. Springer-Verlag, Berlin, 303-313.

Crossref

Google Scholar

[27]

SHAPIRO, E. 1989. The family of concurrent logic programming languages. ACM Comput. Surv. 21, 3 (Sept.), 413-510.

Crossref

Google Scholar

[28]

TURNER, D. T. 1996. The polymorphic pi-calculus: Theory and implementation. Ph.D. thesis, Univ. of Edinburgh, Edinburgh, Scotland.

Google Scholar

[29]

VASCONCELOS, V. T. AND HONDA, K. 1993. Principal typing schemes in a polyadic 7r-calculus. In Proceedings of CONCUR'93. Lecture Notes in Computer Science, vol. 715. Springer-Verlag, Berlin, 524-538.

Crossref

Google Scholar

[30]

WALKER, D. 1995. Objects in the 7r-calculus. Inf. Comput. 116, 253-271.

Crossref

Google Scholar

[31]

YONEZAWA, A. AND TOKORO, M. 1987. Object-Oriented Concurrent Programming. The MIT Press, Cambridge, Mass.

Crossref

Google Scholar

[32]

YOSHIDA, N. 1996. Graph types for monadic mobile processes. In Proceedings of FST/TCS'16. Lecture Notes in Computer Science, vol. 1180. Springer-Verlag, Berlin, 371-387. Full version as LFCS report, ECS-LFCS-96-350, Univ. of Edinburgh.

Crossref

Google Scholar

Cited By

View all

Hirschkoff DPrebet ESangiorgi DGorla D(2021)On sequentiality and well-bracketing in the π-calculusProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470559(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470559
Kokke WDardha O(2021)Prioritise the Best VariationFormal Techniques for Distributed Objects, Components, and Systems10.1007/978-3-030-78089-0_6(100-119)Online publication date: 14-Jun-2021
https://dl.acm.org/doi/10.1007/978-3-030-78089-0_6
Barbanera FLanese ITuosto E(2020)Composing Communicating Systems, SynchronouslyLeveraging Applications of Formal Methods, Verification and Validation: Verification Principles10.1007/978-3-030-61362-4_3(39-59)Online publication date: 20-Oct-2020
https://dl.acm.org/doi/10.1007/978-3-030-61362-4_3
Show More Cited By

Index Terms

A partially deadlock-free typed process calculus
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
    2. General programming languages
      1. Language features
2. Theory of computation
  1. Formal languages and automata theory

Recommendations

An Implicitly-Typed Deadlock-Free Process Calculus
CONCUR '00: Proceedings of the 11th International Conference on Concurrency Theory

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 about concurrent programs by guaranteeing that communication on ...
A Partially Deadlock-free Typed Process Calculus
LICS '97: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science

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 the order of channel use as type information, and (2) classification of ...
Typed closure conversion for the calculus of constructions
PLDI '18

Dependently typed languages such as Coq are used to specify and verify the full functional correctness of source programs. Type-preserving compilation can be used to preserve these specifications and proofs of correctness through compilation into the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 20, Issue 2

March 1998

224 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/276393

Editor:
William Pugh
Univ. of Maryland, College Park

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 March 1998

Published in TOPLAS Volume 20, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

79
Total Citations
View Citations
713
Total Downloads

Downloads (Last 12 months)101
Downloads (Last 6 weeks)29

Reflects downloads up to 28 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Hirschkoff DPrebet ESangiorgi DGorla D(2021)On sequentiality and well-bracketing in the π-calculusProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470559(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470559
Kokke WDardha O(2021)Prioritise the Best VariationFormal Techniques for Distributed Objects, Components, and Systems10.1007/978-3-030-78089-0_6(100-119)Online publication date: 14-Jun-2021
https://dl.acm.org/doi/10.1007/978-3-030-78089-0_6
Barbanera FLanese ITuosto E(2020)Composing Communicating Systems, SynchronouslyLeveraging Applications of Formal Methods, Verification and Validation: Verification Principles10.1007/978-3-030-61362-4_3(39-59)Online publication date: 20-Oct-2020
https://dl.acm.org/doi/10.1007/978-3-030-61362-4_3
Barbanera FLanese ITuosto E(2020)Choreography AutomataCoordination Models and Languages10.1007/978-3-030-50029-0_6(86-106)Online publication date: 15-Jun-2020
https://dl.acm.org/doi/10.1007/978-3-030-50029-0_6
Scalas AYoshida NBenussi EMcKinley KFisher K(2019)Verifying message-passing programs with dependent behavioural typesProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3322484(502-516)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3322484
Lanese ISangiorgi DZavattaro G(2019)Playing with Bisimulation in ErlangModels, Languages, and Tools for Concurrent and Distributed Programming10.1007/978-3-030-21485-2_6(71-91)Online publication date: 3-Jul-2019
https://doi.org/10.1007/978-3-030-21485-2_6
Charalambides MPalmskog KAgha G(2019)Types for Progress in Actor ProgramsModels, Languages, and Tools for Concurrent and Distributed Programming10.1007/978-3-030-21485-2_18(315-339)Online publication date: 3-Jul-2019
https://doi.org/10.1007/978-3-030-21485-2_18
Dardha OGay S(2018)A New Linear Logic for Deadlock-Free Session-Typed ProcessesFoundations of Software Science and Computation Structures10.1007/978-3-319-89366-2_5(91-109)Online publication date: 14-Apr-2018
https://doi.org/10.1007/978-3-319-89366-2_5
Kobayashi NLaneve C(2017)Deadlock analysis of unbounded process networksInformation and Computation10.1016/j.ic.2016.03.004252:C(48-70)Online publication date: 1-Feb-2017
https://dl.acm.org/doi/10.1016/j.ic.2016.03.004
Hüttel HLanese IVasconcelos VCaires LCarbone MDeniélou PMostrous DPadovani LRavara ATuosto EVieira HZavattaro G(2016)Foundations of Session Types and Behavioural ContractsACM Computing Surveys10.1145/287305249:1(1-36)Online publication date: 5-Apr-2016
https://dl.acm.org/doi/10.1145/2873052
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

References

Cited By

Index Terms

Recommendations

An Implicitly-Typed Deadlock-Free Process Calculus