formal systems to specify properties of objects

Type theory is the study of formal systems that classify objects into categories. It was historically introduced in logic, to provide a foundational set theory, and is now widely used in programming language design. Use this tag if your question touches on theoretical aspects of types. For questions about implementing a type system in a programming language, see (there is some overlap).