next up previous contents index
Next: Formal Definition of Up: The Rules Previous: Judgements

The Type System in Detail

This section may be skipped on the first reading, as the informal description of the type system given in section gif should meet the needs of most readers.

This section consists of two parts. First, we give the formal definition of 's type system by means of a recursive  definition of the necessary predicates. Then, for ease of understanding and reference, from the definition we extract criteria for typehood and membership. Those who do read this section may benefit by reading the latter part first.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995