For questions on the formal system in mathematical logic for expressing effective functions, programs and computation, and proofs, using abstract notions of functions and combining them through binding and substitution.

# Lambda Calculus

Its dynamics is a rewriting system representing computation by mean of the beta-reduction, that substitutes each occurrence of the variable with the argument term. From this operational point of view, it represents the ideal formal model of a functional programming language and it can be enriched with constant values and datatypes. Such a typed restriction constitutes the bridge across logic's proof-theory and computer science's theory of computability known as the Curry-Howard correspondence: a term is a proof of its type formula.

## Bibliography

- Henk Barendregt,
*Lambda Calculus. Its Syntax and Semantics*, 1981. The monograph of the subject.