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
The book
Practical Foundations for Programming Languages
Cambridge University Press (2016)
lays the foundations of the theory of programming languages in terms of type theory. In over 500 pages, the author formally specifies and step-by-step extends established type systems and reasons about type safety and operational semantics (not so much dependent types and categorical semantics). The book also contains a discussion of logic in type theory and features of variants of the Algol programming language, in particular.
The preview of the second edition (2016) is available as a pdf. A description of the changes is here.
Practical Foundations of Mathematics
(web)
William Lawvere, Robert Rosebrugh,
Cambridge UP 2003 (book homepage, GoogleBooks, pdf)