Extensions of Fsub with Decidable Typing

Dear Phil,

I'd greatly appeciate it if you would announce the following paper.



The following paper

	Extensions of Fsub with Decidable Typing

		    by Sergei Vorobyov

is now available by anonymous ftp.

FTP instructions:

    ftp ftp.loria.fr
    login: anonymous
    password: <your mail address>
    cd pub/loria/prograis/vorobyov
    get FsubDecTyping.dvi.Z  (or FsubDecTyping.ps.Z)



Abstract. Both subtyping and typing relations in the system Fsub,
the well-known second-order polymorphic typed lambda-calculus with
subtyping [Cardelli-Wegner 85], [Bruce-Longo 90],
[Breazu-Coquand-Gunter-Scedrov 91], [Curien-Ghelli 92],
[Cardelli-Martini-Mitchell-Scedrov 94] appeared to be undecidable
[Pierce 92]. We demonstrate an infinite class of extensions of the
system Fsub, where both relations are decidable. Our
extensions are based on the converging hierarchies of decidable
extensions of the Fsub-subtyping relation (announced earlier).

Every system G from the class satisfies the following properties:

1) all subtyping and typing judgments provable in Fsub are also
G-provable; in particular, every Fsub-typable term is G-typable,
but not conversely: an Fsub-typable term may have additional types in
G, and there exist G-typable terms that are not Fsub-typable;

2) the G-canonical types, analogous to the Fsub-minimum types
[Curien-Ghelli 92], are {\em effectively computable} (as opposed to
Fsub); there exists a decision procedure, which given a context Gamma
and a term t always terminates yielding the G-canonical type 
mu(Gamma |- t) of t in Gamma whenever it exists, and the result
"undefined" otherwise; canonical types are used to decide the typing
relation: Gamma |- t : tau iff Gamma |- mu(Gamma |- t) <: tau;

3) the resulting decidable} G-canonical typing relation extends the
Fsub-minimum typing relation: if sigma is the minimum type of t in
Gamma wrt Fsub, then mu(Gamma |- t) = sigma in G, but not conversely,
in general, since the Fsub-minimum typing relation is undecidable.

Additionally, as every decidable extension of the undecidable Fsub
should inevitably prove ``senseless'' Fsub-unprovable judgments, we
show that there exist extensions G approximating Fsub with any desired

We investigate the properties of the G-typing relation. We prove, in
particular, the G-typing proof normalization theorem, which gives
conditions guaranteeing that a given typing proof in an extension can
be transformed to a unique canonical form. It turns out that some
G-typing proofs fail to normalize, and sometimes the minimum type
property, valid for Fsub [Curien-Ghelli92], fails in the extensions.
But we show that these pathological cases are {\em harmless},
corresponding to the Fsub-untypable (i.e., senseless) terms; so they
can be ignored without influencing the decidability of typing in