[TYPES] Paper on subtyping for pi

[Giuseppe Castagna]

Dear listers,

we would like to announce the avaibility of the following paper

	       Semantic subtyping for the pi-calculus
	    by G. Castagna, R. De Nicola, and D. Varacca

at  http://www.cduce.org/papers/semantic_pi.pdf

All comments are warmly welcome.

			      ABSTRACT				
    Subtyping relations for the pi-calculus are usually  defined in a
syntactic way, by means of  structural rules.  We propose a semantic
characterisation of channel  types and use it to  derive a subtyping
relation.   The  type  system  we consider  includes  read-only  and
write-only channel types, product types, recursive types, as well as
unions, intersections, and negations  of types which are interpreted
as  the  corresponding   set-theoretic  operations.   We  prove  the
decidability  of  the  subtyping  relation,  formally  describe  the
subtyping  algorithm,  and use  the  techniques  developped for  the
decidability of  subtyping to prove  the decidability of  the typing
relation.

In order to fully exploit  the expressiveness of the new type system
(which  subsumes several  existing ones),  we endow  the pi-calculus
with structured channels where communication is subjected to pattern
matching that performs dynamic  typecase.  This paves the way toward
a novel integration of  functional and concurrent features, obtained
by combining  the pi-calculus  with CDuce, a  functional programming
language for XML manipulation that is based on semantic subtyping.


regards

Beppe, Rocco, and Daniele