Commit 5b012bdb authored by Pietro Abate's avatar Pietro Abate
Browse files

[r2004-10-20 14:47:57 by beppe] Empty log message

Original author: beppe
Date: 2004-10-20 14:47:57+00:00
parent b0d1734f
......@@ -118,6 +118,40 @@ Superseded by the previous paper
<paper file="papers/semantic_pi.pdf">
<title>Semantic subtyping for the pi-calculus</title>
<author>G. Castagna</author>
<author>R. De Nicola</author>
<author>D. Varacca</author>
<comment> <i>Unpublished manuscript</i>. </comment>
<abstract> <p>
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
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.
<paper file="papers/">
<title>The Relevance of Semantic Subtyping</title>
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment