# confluence, subject reduction for F^{omega} with products, eta


I would be grateful if anyone could tell me what the status is for:

- confluence
- subject reduction

for Girard's System F^{\omega} extended with products (at both type
and kind level) and *eta-conversion* (for both function and product
types, including the polymorphic Delta).

My understanding (from reading Gallier's excellent tutorial) is that
confluence for $\beta\eta$-conversion is a straightforward application
of Girard's Candidats sur le Reducibilit\'{e}.  My intuition is that
surjective pairing is locally confluent, hence confluence still holds
with surjective pairing.  Am I missing something here?  Are there any
complications for subject reduction?  Is any of this a corollary of
the proof theory worked out for System F with subtyping?

I am aware that matters become mildly nightmarish with dependent
types, I am personally interested in just the system described above.

Citable references would be very much appreciated, thanks
--dd

Spoken: Dominic Duggan	Internet: dduggan@uwaterloo.ca
Canada:	Dept of Computer Science, University of Waterloo,