The type language to be considered in this section consists of a small set of atomic types, and is closed under the binary operations product, left and right division. Some notational conventions: in the specification below, lower case p ranges over atomic types, upper case A, B over arbitrary types. We pronounce A\B as ‘A under B’ and B/A as ‘B over A’ thus to make clear which part of the ‘fraction’ is the denominator (A), and which is the numerator (B).  