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.
See a separate page for semantics of a programming language.
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 theory is 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.
Last revised on December 9, 2020 at 05:39:51. See the history of this page for a list of all contributions to it.