Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Church's formal system used in computatability, programming languages and proof theory to represent effective functions, programs and their computation, and proofs.

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.


  1. Henk Barendregt, Lambda Calculus. Its Syntax and Semantics, 1981. The monograph of the subject.
history | excerpt history