Church devised the lambda calculus, a remarkably simple calculus for studying the nature of mathematical operations. It is now one of the fundamental tools of computer science.
He also stated “Church’s Thesis”, which proposed an exact formalisation for the notion of a class of problems that can be solved by a mechanical method of computation. Thanks to the work of Church’s students Kleene and Turing, his work which led almost directly to John von Neumann’s design for the first electronic digital computers.
Church’s later work shed light on basic issues in logic. He worked on the theory of types which were needed for functional programing languages. His lambda calculus influenced the design of the LISP programming language and functional programming languages in general.