syntax

**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**

Syntax is the formal specification of a theory of formal logic, as opposed to semantics.

Last revised on June 30, 2014 at 11:58:18. See the history of this page for a list of all contributions to it.