### Intrinsic and Extrinsic Semantics of Intersection Types

A definition of a typed language is said to be "intrinsic" if it
assigns meanings to typings rather than arbitrary phrases, so that
ill-typed phrases are meaningless. In contrast, a definition is said
to be "extrinsic" if all phrases have meanings that are independent of
their typings, while typings represent properties of these meanings.

In this talk, we will illustrate both kinds of definitions for a
purely functional language with intersection types that is a
sublanguage of the Forsythe programming language. As with Forsythe,
the intrinsic definition will use limits in a category, but now this
will be a category of algebraic lattices rather than a functor
category.

We will also give a domain-theoretic definition of the corresponding
untyped language, and establish logical relations between these
definitions. Finally, we will define embedding-retraction pairs
between the typed and untyped semantics, prove that these pairs
"bracket" the logical relations, and use this fact to derive an
extrinsic semantics, in which types denote partial equivalence
relations.

July 26, 2000

3:30pm

Wean Hall 8220