In many ways the formalism presented here will resemble a functional programming
language with a rich type structure.
The functions of
are denoted by lambda expressions, written 
x.t,
and correspond to programs.
The function terms do not carry any type information, and they are evaluated
without regard to types.
This is the evaluation style of ML [Gordon, Milner, & Wadsworth 79], and it contrasts with a style in which
some type correctness is checked at runtime (as in PL/I).
The programs of
are rather simple in comparison to those of modern
production languages; there is no concurrency,
and there are few mechanisms to
optimize the evaluation (such as alternative parameter passing mechanisms,
pointer allocation schemes, etc.).
The type structure of is much richer than that of any programming language; for example, no such language offers dependent products, sets, quotients and universes. On the other hand, many of the types and type constructors familiar from languages such as Algol 68, Simula 67, Pascal and Ada are available in some form in
. We discuss this briefly below.
A typical programming language will have among its primitive types the
integers, int, booleans, bool, characters, char, and
real numbers (of finite precision), real.
In
the type of integers, int, is provided; the booleans can be
defined using the set type as
{x:int | x=0 in int or x=1 in int},
the characters are given by atom, and various kinds of real numbers can be
defined (including infinite precision), although
no built--in finite precision
real type is as yet provided.
Many programming languages provide ways to build tuples of values.
In Algol the constructor is the structure; in Pascal and Ada it is the
record and has
the form 
for the product of types A and B.
In
such a product would be written A#B just as it would be in ML.
In Pascal the variant record has the following form.
RECORD
CASE kind:(RECT,TRI,CIRC) of
RECT:(w,h:real);
CIRC:(r:real);
TRI :(x,y,a:real)
END
The elements of this type are either pairs, triples or quadruples, depending
on the first entry.
If the first entry is RECT then there are two more components,
both reals.
If the first entry is CIRC then there is only one other which is a real; if
it is TRI then there are three real components.
One might consider this type a discriminated union rather than a
variant record.
In any case, in
it is defined as an extension of the product operator which
we call a dependent product.
If real denotes the type of finite precision reals, and if the Pascal
type (RECT,CIRC,TRI) is represented by the type consisting of the three atoms
"RECT","CIRC" and "TRI", and if the function F is defined as
F("RECT") = real#real
F("CIRC") = real
F("TRI") = real#real#real
then the following type represents the variant record.
i:("RECT","CIRC","TRI")#F(i)
In , as in Algol 68 , it is possible to form directly the disjoint union , written A|B, of two types A and B. This constructor could also be used to define the variant record above as real#real|(real|real#real#real).
One of the major differences between types and those of most programming languages is that the type of functions from A to B, written A->B, denotes exactly the total functions. That is, for every input a of type A, a function in A->B must produce a value in B. In Algol the type of functions from A to B, say PROC(x:A)B, includes those procedures which may not be well--defined on all inputs of A; that is, they may diverge on some inputs.
In contrast to the usual state of affairs with programming languages the semantics of ``programs'' is completely formal. There are rules to settle such issues as when two types of programs are equal, when one type is a subtype of another, when a ``program'' is correctly typed, etc. There are also rules for showing that ``programs'' meet their specifications. Thus is related to programming languages in many of the ways that a programming logic or program verification system is.