Lambda calculus and intuitionistic linear logic

The Curry-Howard isomorphism 1 is the basis of typed functional programming. By means of this isomorphism, the intuitionistic proof of a formula can be seen as a functional program, whose type is the formula itself. In this way, the computation process has its logic realization in the proof normalization procedure. Both the implicative fragment of the intuitionisti