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.
The Lambda Calculus, its Syntax and Semantics
Lambda Calculi with Types
Proof-assistants using Dependent Type Systems (with H. Geuvers)
Problems in Type Theory