Safe sound type system

A Type system where the static judgment "term $t$ has type $T$" implies a corresponding semantic property at runtime - formalized as: if the type system accepts a program, execution cannot produce behaviors the types claim to exclude.

A type system where the static judgment "term $t$ has type $T$" implies a corresponding semantic property at runtime - formalized as: if the type system accepts a program, execution cannot produce behaviors the types claim to exclude.