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.
Chapter PDF
Similar content being viewed by others
References
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.
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.
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.
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.
Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17(3):348–375, December 1978.
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.
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.
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.
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.
Andrew K. Wright. Simple imperative polymorphism. Lisp and Symbolic Computation, 8(4):343–356, December 1995.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Conchon, S., Pottier, F. (2001). JOIN(X): Constraint-Based Type Inference for the Join-Calculus. In: Sands, D. (eds) Programming Languages and Systems. ESOP 2001. Lecture Notes in Computer Science, vol 2028. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45309-1_15
Download citation
DOI: https://doi.org/10.1007/3-540-45309-1_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41862-7
Online ISBN: 978-3-540-45309-3
eBook Packages: Springer Book Archive