It is defined in this paper itself; see section 3 titled &quot;Language,&quot; beginning &quot;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.&quot; Also see figure 5, which is its formal syntax after desugaring.