Fair subtyping is a liveness-preserving refinement relation for session types akin to (but coarser than) the well-known should-testing precongruence. The behavioral characterization of fair subtyping is challenging essentially because fair subtyping is context-sensitive: two session types may or may not be related depending on the context in which they occur, hence the traditional coinductive argument for dealing with recursive types is unsound in general. In this paper we develop complete behavioral and axiomatic characterizations of fair subtyping and we give a polynomial algorithm to decide it.
Fair Subtyping for Open Session Types
PADOVANI, Luca
2013-01-01
Abstract
Fair subtyping is a liveness-preserving refinement relation for session types akin to (but coarser than) the well-known should-testing precongruence. The behavioral characterization of fair subtyping is challenging essentially because fair subtyping is context-sensitive: two session types may or may not be related depending on the context in which they occur, hence the traditional coinductive argument for dealing with recursive types is unsound in general. In this paper we develop complete behavioral and axiomatic characterizations of fair subtyping and we give a polynomial algorithm to decide it.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
