Documentation

This monad denotes computations which produce values at security level l.

This function unlabels data (to be used only by trusted modules)

It raises the security level of a value based on order-relationship expressed by the security lattice.

This is the only operation which connects members of the Sec l monad family.