Also see Types for supplementary material.

The
semantics is a variation on that given by Martin-Löf
for
his type theory [Martin-Löf 82]. There are three stages in the semantic specification:
the
* computation system*,
the * type system* and
the so--called * judgement forms*. Here
is how we shall proceed.
We shall specify a computation system consisting of * terms*,
divided
into * canonical* and
* noncanonical* , and a procedure for
* evaluating*
terms which for a given term **t** returns at most one canonical term,
called the * value* of **t**.
In
whether a term is canonical depends only on the
outermost form of the term, and there are terms which
have no value.
We shall write to mean that **s** has value **t**.

Next we shall specify a system of types. A * type* is a term **T** (of the
computation system) with which is associated a transitive, symmetric
relation, , which respects evaluation in **t** and **s**;
that is, if **T** is a type and and , then if and only if .
We shall sometimes say ``**T** type'' to mean that **T** is a type.
We say **t** is a * member* of **T**, or , if .
Note that is an equivalence relation (in **t** and **s**)
when restricted to members of **T**.
Actually, is a three--place relation on terms which respects evaluation
in all three places. We also use a transitive, symmetric relation on
terms, **T=S**, called * type equality*,
which respects in **T**; that is,
if **T=S** then if and only if .
The relation **T=S** respects evaluation in **T** and **S**,
and **T** is a type if and only if **T=T**.
The restriction of **T=S** to types is an equivalence relation.

For our purposes, then, a type system for a given
computation system
consists of a two--place relation **T=S** and a three--place relation
on terms such that

We define ``T=Sis transitive and symmetric;

T=Sif and only if & ;

is transitive and symmetric intands;

if and only if & ;

T=Tif ;

ifT=S& .

Ttype if and only ifT=T;

if and only if .

Finally, so--called judgements will be explained. This requires
consideration of terms with free variables
because substitution of closed
terms for free variables is central to judgements as presented
here.
In the description of semantics given so far
``term'' has meant a closed term, i.e., a term with no free variables.
There is only one form of judgement in
,
` :,,: >> S [ext s]`,
which in the case that

Thu Sep 14 08:45:18 EDT 1995