Proofs and programs (Q1408657)

This paper is a general presentation, very readable, of the use of \(\lambda\)-calculus as a system of notations for proofs. As said in the introduction, this can help in the design of interactive proof systems for making computers do mathematics, complementary to computer algebra systems that aid algebraists or analysts in doing computations. Various relevant aspects of the theory of \(\lambda\)-calculus are presented: \(\lambda\)-calculus notation for proofs in natural deduction, Hindley-Milner algorithm, semantics of \(\lambda\)-calculus, polymorphism and its semantics.