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) ENDThe elements of this type are either pairs, triples or quadruples, depending on the first entry. If the first entry is

F("RECT") = real#real F("CIRC") = real F("TRI") = real#real#realthen 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

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

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.

Thu Sep 14 08:45:18 EDT 1995