Lambda calculus is a formal language capable of expressing computable functions and also logical proofs.

In combination with types it can denote on the one hand functional programs and on the other hand mathematical proofs.