Thursday 8 December 2022, 14:00, room 3U42 and online: Impredicativity, comprehension scheme, polymorphism and bar recursion, Valentin Blot (Deducteam).
I will present the logical correspondence between impredicatvity and the comprehension scheme, which are the two usual ways of presenting second-order arithmetic. The former, used in type theory, is preferred by computer scientists. The later, used in reverse mathematics, is preferred by mathematicians. Computationally, impredicativity is naturally interpreted via polymorphic types (System F), while the comprehension scheme is usually interpreted via bar recursion and its variants. I will present recent work bridging the gap between the two logical presentations, leading to a closer correspondence between polymorphism and bar recursion.