A sort inference algorithm for the polyadic &pgr;-calculus

ABSTRACT

In Milner's polyadic &pgr;-calculus there is a notion of sorts which is analogous to the notion of types in functional programming. As a well-typed program applies functions to arguments in a consistent way, a well-sorted process uses communication channels in a consistent way. An open problem is whether there is an algorithm to infer sorts in the &pgr;-calculus in the same way that types can be inferred in functional programming. Here we solve the problem by presenting an algorithm which infers the most general sorting for a process in the first-order calculus, and proving its correctness. The algorithm is similar in style to those used for Hindley-Milner type inference in functional languages.

REFERENCES

• Hin69: J.R. Hindley. The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society, 146:29-60, 1969.
• Mil78: R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17, 1978.
• Mil89: R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• Mil91: R. Milner. The polyadic ~r-calculus: A tutorial. Technical report, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, 1991.
• MPW89: R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes. Technical report, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, 1989.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Concurrent programming structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Algorithms, Languages, Theory, Verification