Big-step/Natural operational semantics

A style of semantic which defines evaluation via Evaluation statement/judgement of the form $\begin{array}{l}t\\ Downarrowv\end{array}$, relating a term directly to its final value in a single derivation rather than through int

A style of semantic which defines evaluation via Evaluation statement/judgement of the form $t\Downarrow v$, relating a term directly to its final value in a single derivation rather than through intermediate steps.