On the Meaning of Focalization
Résumé
In this paper, we use Girard’s ludics to analyze focalization, a fundamental property of the proof theory of linear logic. In particular, we show how focalization can be realized interactively thanks to suitable section-retraction pairs between semantical types.