1 Inroduction

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 syntax

ffl typing rules

ffl equational rules

1.1 Syntax

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

and

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.