[PL-sem-jr] Followup on today's talk

[Felix S. Klock II]

> I suspect that principal types are orthogonal to recursive types and maybe 
> we sould see them seperately. By the way, where does barendregt mentions 
> principal types? It's kind of a pain to spot his subsections :-(

Barendregt covers principal types in section 4.4, "Decidability of
type assignment" (see Definition 4.4.9)

The section also covers substitutions, Robinson's unification theorem, 

I'd be curious to know if Barendregt's "principal pairs" are the same
thing as "principal typINGs" that I've seen discussed in the
literature.

-Felix