Caires, L, Seco JC.  2012.  The Type Discipline of Behavioral Separation (Long version with proofs). : CITI / DI-FCT-UNL