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.

References

The Lambda Calculus, its Syntax and Semantics

Lambda Calculi with Types

Proof-assistants using Dependent Type Systems (with H. Geuvers)

Problems in Type Theory