It is defined in this paper itself; see section 3 titled "Language," beginning "In this section we formally define Cogent, including its linear type system, its

It is defined in this paper itself; see section 3 titled "Language," beginning "In this section we formally define Cogent, including its linear type system, its two dynamic semantics — update and value — mentioned earlier in §2, and the refinement theorem between them." Also see figure 5, which is its formal syntax after desugaring.