 Whilst some textbooks on type theory can seem, to the logician, to be rather hazy on exactly which, if any, of the above interpretations of ‘type’ is at issue this is certainly not generally the case with the pioneers of these theories. Howard, for example, writes in his classic paper ‘The Formula-as-Types Notion of Construction’: