Church was an American mathematician and logician who made major contributions to mathematical logic and the foundations of theoretical computer science. He is best known for the lambda calculus, Church's thesis and the Church-Rosser theorem.

In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system designed to investigate function definition, function application and recursion..

In computability theory the Church–Turing thesis (also known as Church's thesis, Church's conjecture and Turing's thesis) is a combined hypothesis about the nature of effectively calculable (computable) functions by recursion (Church's Thesis), by mechanical device equivalent to a Turing machine (Turing's Thesis) or by use of Church's λ-calculus:

The Church–Rosser theorem states that if there are two distinct reductions starting from the same lambda calculus term, then there exists a term that is reachable via a (possibly empty) sequence of reductions from both reducts.