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
Substructural logic is a general term for logics in which the structural rules:
the contraction rule
the weakening rule
the exchange rule
are not necessarily allowed, or are only allowed with restrictions.
Some particular substructural logics include:
Last revised on March 30, 2023 at 08:34:40. See the history of this page for a list of all contributions to it.