JOIN(X): Constraint-Based Type Inference for the Join-Calculus - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2001

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

Résumé

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 semi-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. This hybrid approach allows giving pleasant logical meaning to high-level notions such as type variables, constraints and generalization, and clearly separating them from low-level aspects (substitution lemmas, etc.), which are dealt with in a simple, standard way.
Fichier principal
Vignette du fichier
conchon-fpottier-esop01.pdf (309.53 Ko) Télécharger le fichier

Dates et versions

inria-00000029 , version 1 (16-05-2005)

Identifiants

  • HAL Id : inria-00000029 , version 1

Citer

Sylvain Conchon, François Pottier. JOIN(X): Constraint-Based Type Inference for the Join-Calculus. Proceedings of the 10th European Symposium on Programming (ESOP'01), Apr 2001, Genova, pp.221--236. ⟨inria-00000029⟩

Collections

INRIA INRIA2
111 Consultations
82 Téléchargements

Partager

Gmail Facebook X LinkedIn More