Advertisement

JOIN(X): Constraint-Based Type Inference for the Join-Calculus

  • Sylvain Conchon
  • François Pottier
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2028)

Abstract

We present a generic constraint-based type system for the join-calculus. The key issue is type generalization, which, in the presence of concurrency, must be restricted.We first define a liberal generalization criterion, and prove it correct. Then, we find that it hinders type inference, and propose a cruder one, reminiscent of ML’s value restriction. We establish type safety using a emsemi-syntactic technique, which we believe is of independent interest. It consists in interpreting typing judgements as (sets of) judgements in an underlying system, which itself is given a syntactic soundness proof.

References

  1. [1]
    Sylvain Conchon and Fabrice Le Fessant. Jocaml: Mobile agents for Objective-Caml. In First International Symposium on Agent Systems and Applications and Third International Symposium on Mobile Agents (ASA/MA’99), pages 22–29, Palm Springs, California, October 1999. URL: http://para.inria.fr/~conchon/publis/asa99.ps.gz.
  2. [2]
    Sylvain Conchon and François Pottier. JOIN(X): Constraint-based type inference for the join-calculus. Long version. URL: http://pauillac.inria.fr/ fpottier/publis/ conchon-fpottier-esop01-long.ps.gz, April 2001.
  3. [3]
    Cédric Fournet and Georges Gonthier. The reflexive chemical abstract machine and the join-calculus. In Proceedings of the 23rd ACM Symposium on Principles of Programming Languages, pages 372–385, 1996. URL: http://pauillac.inria.fr/~fournet/papers/popl-96.ps.gz.
  4. [4]
    Cédric Fournet, Luc Maranget, Cosimo Laneve, and Didier Rémy. Implicit typing la ML for the join-calculus. In 8th International Conference on Concurrency Theory (CONCUR’97), volume 1243 of Lecture Notes in Computer Science, pages 196–212, Warsaw, Poland, 1997. Springer. URL: ftp://ftp.inria.fr/INRIA/Projects/Didier.Remy/cristal/typing-join.ps.gz.Google Scholar
  5. [5]
    Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17(3):348–375, December 1978.zbMATHCrossRefMathSciNetGoogle Scholar
  6. [6]
    Martin Odersky, Martin Sulzmann, and Martin Wehr. Type inference with constrained types. Theory and Practice of Object Systems, 5(1):35–55, 1999. URL: http://www.cs.mu.oz.au/~sulzmann/publications/tapos.ps.CrossRefGoogle Scholar
  7. [7]
    Martin Odersky, Christoph Zenger, Matthias Zenger, and Gang Chen. A functional view of join. Technical Report ACRC-99-016, University of South Australia, 1999. URL: http://lampwww.epfl.ch/~czenger/papers/tr-acrc-99-016.ps.gz.
  8. [8]
    Martin Sulzmann. A general framework for Hindley/Milner type systems with constraints. PhD thesis, Yale University, Department of Computer Science, May 2000. URL: http://www.cs.mu.oz.au/~sulzmann/publications/diss.ps.gz.
  9. [9]
    Martin Sulzmann, Martin Müller, and Christoph Zenger. Hindley/Milner style type systems in constraint form. Research Report ACRC-99-009, University of South Australia, School of Computer and Information Science, July 1999. URL: http://www.ps.uni-sb.de/~mmueller/papers/hm-constraints.ps.gz.
  10. [10]
    Andrew K. Wright. Simple imperative polymorphism. Lisp and Symbolic Computation, 8(4):343–356, December 1995.CrossRefGoogle Scholar
  11. [11]
    Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, November 1994. URL: http://www.cs.rice.edu/CS/PLT/Publications/ic94-wf.ps.gz.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Sylvain Conchon
    • 1
  • François Pottier
    • 1
  1. 1.INRIARocquencourt

Personalised recommendations