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
De Bruijn indices are used to represent terms in lambda calculus without naming bound variables.
Created on June 2, 2022 at 22:16:58. See the history of this page for a list of all contributions to it.