The simply-typed -calculus is one of the simplest type systems studied in logic and programming languages. It can be used for many things, including amongst others:
An classic introduction to the typed -calculus as a core programming languages is contained in the first part of Benjamin Pierce's Types and Programming Languages.
The simply-typed -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}
}
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}
}