Skip to content
scrambled
Programming Language Theory Concept

Safe/Sound type system

Books JourneyProgramming Language Theory Statuslearning

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.