natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
Semantics is the interpretation of the syntax of a theory in a model.
Notably the semantics of type theories is given by categories. For instance
dependent type theory is precisely the formal language for which locally cartesian closed categories are the semantics,
intensional type theoryis the formal language for which locally cartesian closed (infinity,1)-categories are the semantics;
homotopy type theory is the formal language for which elementary (infinity,1)-toposes are the semantics.
For more on this see at categorical semantics and at relation between type theory and category theory.