Аннотация:We introduce a natural deduction formulation for the Logic of Proofs, a refinement of modal logic S4 in which the assertion square A is replaced by [s]A whose intended reading is "s is a proof of A". A term calculus for this formulation yields a typed lambda calculus lambda(I) that internalises intensional information on how a term is computed. In the same way that the Logic of Proofs internalises its own derivations, lambda(I) internalises its own computations. Confluence and strong normalisation of lambda(I) is proved. This system serves as the basis for the study of type theories that internalise intensional aspects of computation.