type preservation

Type preservation is an important property of a type system and operational semantics. Informally, an operational semantics $t \longrightarrow t\prime$ preserves types if the evaluation of $t$ does not change its type.

More formally, if $\Gamma \vdash t : A$ and $t \longrightarrow t\prime$, then $\Gamma \vdash t\prime : A$.

Created on October 6, 2017 at 11:22:10. See the history of this page for a list of all contributions to it.