The calculi under investigation are
ffl the simply typed >=-calculus with constants and products called >=?.
ffl the simply typed >=-calculus with constants, products and fixpoint operators called >= ? Y
ffl the recursively typed >=-calculus called Y>=?
They are treated in the general framework of type theories, i.e they decompose into
ffl typing rules
ffl equational rules
The description of the syntax consists of two sets of BNF-productions, one for the syntax of the types and the other for the syntax of the terms.
1.2 Typing rules
For each calculus there is a enumerable set of variables V, a enumerable set of constants C and a collection of types T which may be a proper class. A typing context H consists of two partial functions
HV : V ! T
HC : C ! T
Hv and Hc have finite domains and often written as lists. At a first glance it seems artificial to split a typing context in a variable and a constant part. However, the latter come from a different syntax class and, in particular, cannot be bound by abstractions like the former. A typing judgement H ` M : t means that the term M has the type t relative to the typing context H. A typing rules consist of a finite number of typing judgements as premisses and a conclusion, often written
H1 ` M1 : t1; : : : ; H1 ` Mn : tn
H ` M : t
The typing rules define an inference system. where a proof of H ` M : t is called a typing derivation. It certifies that a term is well-typed and only welltyped terms are given a meaning in a semantic model.