Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
9655875 | Electronic Notes in Theoretical Computer Science | 2005 | 16 Pages |
Abstract
We introduce channel sequence types to study finitary polymorphism in the context of mobile processes modelled in the Ï-calculus. We associate to each channel a set of exchange types, and we require that output processes send values of one of those types, and input processes accept values of any type in the set. Our type assignment system enjoys subject reduction and guarantees the absence of communication errors. We give several examples of polymorphism, and we encode the λ-calculus with the strict intersection type discipline.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Sergio Maffeis,