Proofs of propositional calculus may be written in simple typed lambda calculus(λ→). (as shown on p.52-53 in https://www.cs.ru.nl/~freek/talks/lc-2012/lambda5.pdf ) I think that this calculus may be enriched with 0,1,*, + and constant c:A\/~A for proofs of classical reasoning, which represents(roughly) contradiction, truth, concatenation of proofs, combining of proofs and LEM.
1) Could you please recommend me a paper which contains detailed presentation of such enriched calculus?
2) I am also interested in similar calculus but for predicate calculus. If it exists, how it is called, which paper about it should I read?
This question hints at a lot of major mathematics, as the intersection of lambda calculus, type theory, and logic is a major talking point right now.
One point you are sure to run into when reading about this is the LEM - most people working in type theoretic logics prefer to forgo the LEM. Intuitively this is because we want a very strong form of disjunction, which says that we must have proven either $A$ or $B$ in order to conclude $A \lor B$. This is in direct opposition with the idea that we can know $A \lor ~A$ without having proven either!
In this vein, here is a lovely set of lecture notes from a logic class at CMU which explains what you are after (without the LEM). It is from 15-317, Constructive Logic, and the website is here in case you want to read more.
If you insist upon having LEM, there are a few avenues available. Here is another set of lecture notes from a prior iteration of the same course, which discusses classical logic. For completeness, here is the website from this iteration of the course.
As for quantification, here is another set of lecture notes from the same course which talks about one approach.
If you are interested in lambda terms acting as witnesses for the truth of propositions, Type Theory is a worthwhile keyword to start searching! There are two sides to the type theoretic coin, with proof theory on the math side, and programming language theory on the other. You can find information about both here. It is a github repo including PDFs relating to type theory, subcategorized by topic!
An excellent reference for the proof theoretic side of Type Theory is Proofs and Types by Girard. I've also been told Type Theory and Formal Proof, by Nederpelt and Geuvers is good, though I have not read it.
As for programming language theory, I cannot recommend Practical Foundations for Programming Languages by Harper highly enough. It is excellently written (if extremely opinionated), and does a good job surveying the entire field.
Finally I feel personally obligated to mention Martin-Lof type theory, which serves as a potential replacement for set theory as the foundation of mathematics. It is a dependent theory, which requires some care in setting up. The results, however, are beautiful. If you have a background in Algebraic Topology, The HoTT Book is an excellent example of Martin-Lof type theory in the wild.
I hope this helps ^_^