nLab
type preservation

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

More formally, if Γt:A\Gamma \vdash t : A and ttt \longrightarrow t\prime, then Γt:A\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.