Abstract:
Session types are used to describe and structure interactions between
independent processes in distributed systems. Higher-order types are needed in
order to properly structure delegation of responsibility between processes. In this
paper we show that higher-order web-service contracts can be used to provide
a fully-abstract model of recursive higher-order session types. The model is settheoretic,
in the sense that the denotation of a contract is given by the set of
contracts with which it complies; we use a novel notion of peer compliance. A
crucial step in the proof of full-abstraction is showing that every contract has a
non-empty denotation.
