This post is based on the paper by Thomas Austin and Cormac Flanagan.
A value can be read by some entity who has the proper authority to read it. A value <k ? s : p> means an entity with authority label k or higher will see the value s, otherwise it will see p.
They have evaluation semantics for faceted values. And they also have a concept of view.
L: Faceted_Value → value
Equivalnce of view, if V1 eqv V2 then L(V1) = L(V2)
start from section 3.2