Simply-typed \lambda-calculus

The simply-typed \lambda-calculus is one of the simplest type systems studied in logic and programming languages. It can be used for many things, including amongst others:

as a very small, core programming language (with limited expressivity)
as a language for defining functions as rules
as a 'substrate' for higher-order logic

References

Wikipedia page
An classic introduction to the typed \lambda-calculus as a core programming languages is contained in the first part of Benjamin Pierce's Types and Programming Languages.
The simply-typed \lambda-calculus was introduced in

Church, Alonzo. 1940. ‘A Formulation of the Simple Theory of Types’. The Journal of Symbolic Logic 5 (02): 56–68. https://doi.org/10.2307/2266170.

@article{church_1940,
	title = {A formulation of the simple theory of types},
	volume = {5},
	url = {www.jstor.org/stable/2266170},
	doi = {10.2307/2266170},
	number = {02},
	journal = {The Journal of Symbolic Logic},
	author = {Church, Alonzo},
	year = {1940},
	pages = {56--68}
}

A classic survey introduction is given in the chapter

Barendregt, Henk. 1993. ‘Lambda Calculus with Types’. In Handbook of Logic in Computer Science, edited by S. Abramsky, Dov M. Gabbay, and T. S. E. Maibaum. Vol. 2. Oxford: Clarendon Press. pdf

@incollection{barendregt_1993,
	address = {Oxford},
	title = {Lambda {Calculus} with {Types}},
	volume = {2},
	booktitle = {Handbook of {Logic} in {Computer} {Science}},
	publisher = {Clarendon Press},
	author = {Barendregt, Henk},
	editor = {Abramsky, S. and Gabbay, Dov M. and Maibaum, T. S. E.},
	year = {1993}
}