Approaching Girard's functor Lambda

Girard has claimed that $\Pi^1_1$-comprehension corresponds to his functor Lambda on dilators. He described a plausible proof around 1980, but it seems that details remain difficult. This talk presents joint work with Aguilera and Weiermann, in which we give a detailed proof that $\Pi^1_1$-comprehension corresponds to a variant of Lambda, namely the functor $\mathbb J$ of Päppinghaus. No prior knowledge of dilators is assumed.