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
basic constructions:
strong axioms
In the general context of foundations of mathematics in practical foundations (following a term introduced in (Taylor)) the emphasis is on conceptually natural formalizations that concentrate the essence of practice and in turn use the result to guide practice (Lawvere), as in (Eilenberg-Steenrod, Harper).
Formal systems of interest here are natural deduction in type theories?, which allow natural expressions for central concepts in mathematics (notably via their categorical semantics and the conceptual strength of category theory).
Under computational trinitarianism this corresponds to a practical foundation in programming, laid out in
A foundation for algebraic topology is this practical spirit is laid out in