= Type safety
{wiki}
For a specified <programming language> and execution model, <type safety> commonly follows from two properties: a closed expression satisfying a <typing judgment> is either a value or can take an execution step, and taking a step preserves its type. Proofs proceed by <structural induction> on derivations, using <capture-avoiding substitution> for function calls. Repeated preservation keeps the remaining expression typed; the first property then rules out getting stuck at an operation outside the model's permitted cases. This argument does not imply termination or correctness of an arbitrary specification. https://softwarefoundations.cis.upenn.edu/plf-current/Types.html[Software Foundations, Programming Language Foundations, Type Systems: progress, preservation and type soundness]{ref}
Back to article page
