seminaire PPS Jeudi 25/6

Chers tous,
le prochaine seminaire PPS est

Jeudi 25 Juin, 11h, salle 0C2:

Colin Riba (ENS Lyon)

On the Values of Reducibility Candidates

Abstract:
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.