de Mathématiques de Luminy
Regnier Laurent and Urzyczyn
Retractions of types with many atoms.
We define a sound and complete proof system for affine -retractions in simple types (built over many atoms), and we state a necessary condition for arbitrary -retractions in simple types. We also show a simple necessary condition for polymorphic -retractability and we disprove an earlier conjecture about a stronger necessary condition.