[Prev][Next][Index][Thread]
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,
Waterloo, Ontario, Canada N2L 3G1