Implicit typing à la ML for the join-calculus. (English) Zbl 1512.68057
Mazurkiewicz, Antoni (ed.) et al., CONCUR ’97: concurrency theory. 8th international conference. Warsaw, Poland. July 1–4, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1243, 196-212 (1997).
Summary: We adapt the Damas-Milner typing discipline to the join-calculus. The main result is a new generalization criterion that extends the polymorphism of ML to join-definitions. We prove the correctness of our typing rules with regard to a chemical semantics. We also relate typed extensions of the core join-calculus to functional languages.
For the entire collection see [Zbl 1434.68030].
For the entire collection see [Zbl 1434.68030].
MSC:
| 68N18 | Functional programming and lambda calculus |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
Software:
PictReferences:
| [1] | L. Damas and R. Milner. Principal type schemes for functional programs. In Proceedings on Principles of Programmining Languages, pages 207-212, 1982. |
| [2] | C. Fournet and G. Gonthier. The reflexive chemical abstract machine and the join-calculus. In 23rd ACM Symposium on Principles of Programming Languages (POPL’96), 1996. |
| [3] | C. Fournet, G. Gonthier, J.-J. Lévy, L. Maranget, and D. Rémy. A calculus of mobile agents. In 7th International Conference on Concurrency Theory (CONCUR’96), 1996. LNCS 1119. |
| [4] | N. Kobayashi, B. C. Pierce, and D. N. Turner. Linear types and picalculus. In 23rd ACM Symposium on Principles of Programming Languages (POPL’96), 1996. |
| [5] | K. Läufer and M. Odersky. An extension of ML with first-class abstract types. In Proceedings of the ACM SIGPLAN Workshop on ML and its Applications, 1992. |
| [6] | R. Milner. The polyadic \(π\)-calculus: a tutorial. In Bauer, Brawer, and Schwichtenberg, editors, Logic and Algebra of Specification. Springer Verlag, 1993. |
| [7] | B. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. In Logic in Computer Science, pages 187-215, 1993. |
| [8] | B. Pierce and D. Turner. Pict: a programming language based on the pi-calculus, 1995. To appear. |
| [9] | J. H. Reppy. Concurrent ML: Design, application and semantics. In Programming, Concurrency, Simulation and Automated Reasoning, pages 165-198, 1992. LNCS 693. |
| [10] | B. Thomsen. Polymorphic sorts and types for concurrent functional programs. Technical Report ECRC-93-10, European Computer-Industry Research Center, Munich, Germany, 1993. |
| [11] | D. N. Turner. The π-calculus: Types, polymorphism and implementation. PhD thesis, LFCS, University of Edinburgh, 1995. |
| [12] | V. T. Vasconcelos. Predicative polymorphism in the \(π\)-calculus. In Proceedings of 5th Conference on Parallel Architectures and Languages (PARLE 94), 1994. LNCS. |
| [13] | A. K. Wright. Polymorphism for imperative languages without imperative types. Technical Report 93-200, Rice University, February 1993. |
| [14] | A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38-94, 1994. · Zbl 0938.68559 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
