The following is a short, non-exhaustive selection of references used to ground the terminology of this documentation, listed roughly in order of increasing depth.

Primary Texts

Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002. The standard introduction to type systems; the type-theoretic notation used in the Type Theoretic Foundations mostly follows it.
Robert Harper, Practical Foundations for Programming Languages, 2nd Edition, Cambridge University Press, 2016. A more advanced, judgment-centered account of the same material.
Henk Barendregt, The Lambda Calculus: Its Syntax and Semantics, North-Holland, 1984. The classical reference for lambda terms, hence for the notion of formal variable and abstraction used in the introduction.

The Curry-Howard Correspondence

William A. Howard, "The formulae-as-types notion of construction", in To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism*, Academic Press, 1980.
Philip Wadler, "Propositions as Types", Communications of the ACM 58(12), 2015. An accessible account of the correspondence summarized in the Introduction table.

Grounding of the Glossary

The logical connectives and product/sum notations used in this glossary follow the conventions of the primary texts above and the standard mathematical notation for sets and tuples.
Language-specific terms are grounded in the C++ Vocabulary page, and the terms specific to kumi in the Nomenclature page.