*Abstract:*

We present an *axiomatic* characterization of models
*fully-complete* for *ML-polymorphic types* of System F.
This axiomatization is given for *hyperdoctrine* models, which
arise as *adjoint models*, i.e. *co-Kleisli categories*
of suitable *linear categories*. Examples of adjoint models
can be obtained from categories of *Partial Equivalence
Relations* over *Linear Combinatory Algebras*. We show that
a special linear combinatory algebra of *partial involutions*
induces an hyperdoctrine which satisfies our axiomatization, and
hence it provides a fully-complete model for ML-types.

**ECS-LFCS-99-414**.

This report is available in the following formats:

- PDF file
- Gzipped PDF file
- PostScript file
- Gzipped PostScript file
- PostScript file with Type 1 fonts
- Gzipped PostScript file with Type 1 fonts
- LaTeX DVI file
- Gzipped LaTeX DVI file