\Gamma |- M has type tau should be called a "typing assertion", or to be more Swedish, a "typing judgement". Andy Pitts