Semantics of programs in type theory are most of the time described by a small step relation which describes, possibly non-deterministically, how to perform one

Semantics of programs in type theory are most of the time described by a small step relation which describes, possibly non-deterministically, how to perform one step of computation. Separately one can consider which terms are values, indicating a successful, terminating computation. Type theory would then involve proving properties about the semantics of typed programs. One can give a small step relation for a Turing machine and one could possibly come up for a type system for it, but generally one starts with the semantics for untyped lambda calculus. Some of the more advanced type theory stuff unifies the notions of terms and types, meaning arbitrary computations can happen in type checking and so properties about types can involve properties about computation in general.