From: "Christopher L Conway" <cconway@cs.nyu.edu>

> Do any of these papers address existentials?

There are no existentials in ocaml, only first-class universal types
(in polymorphic methods and polymorphic record fields.)
Universal types can be used to encode existentials through the usual
dual encoding.
The theory behind polymorpic methods is described in my paper with
Didier Remy, in the Objects section. Polymorphic fields in records are
simpler, and they were already formalized in earlier papers by Didier
Remy.

(Actually, abstract types in modules can also be seen as existentials,
but I don't think this is what you are talking about.)

Jacques Garrigue