Sciweavers

TLCA
2009
Springer

On the Values of Reducibility Candidates

14 years 5 months ago
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. Moreover, for extensions of the lambda-calculus based on intuitionistic logic, we show that the obtained existential quantification is equivalent to its usual impredicative encoding w.r.t. provability in realizability models built from reducibility candidates and biorthogonals.
Colin Riba
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where TLCA
Authors Colin Riba
Comments (0)