Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics.