25/6/09 Colin Riba (ENS Lyon)

On the Values of Reducibility Candidates

The straightforward elimination of union types is known to break subject reduction, and for some extensions of the lambda-calculus, to break strong normalization as well. Similarly, the straightforward elimination of implicit existential types breaks subject reduction.

We propose elimination rules for union types and implicit existential quantification which use a form call-by-value issued from Girard's reducibility candidates. We show that these rules remedy the above mentioned difficulties, for strong normalization and, for the existential quantification, for subject reduction as well.