 In natural deduction systems, normalisation is the procedure by which redundant inferential loops are eliminated. In certain logics (such as intuitionistic logic), a normalisation metatheorem holds and tells us that any proof can be stripped of its redundancy and reduced to a normal form. A further level of correspondence, brought out by Howard, links normalisation with the ‘evaluation’ of programs in which complex terms are reduced to their simplest forms (this is not always possible in the more expressively powerful type systems). 