Séminaire PhilMath

Nous aurons le plaisir d'accueillir Marie Kerjean, LIPN, Université Paris 13

∂ IS FOR DIALECTICA : WHEN PROOFS AND PROGRAMS MEET DIFFERENTIATION

which factors through Girard'ss translation, allowing the realization of 
several semi-classical axioms such as Markov’s principle. During this 
talk, we will see how Dialectica identifies with reverse mode automatic 
differentiation, a way of computing efficiently the differential of a 
succession of functions. This talk will be an opportunity to look at 
Dialectica and differentiation through the lens of denotational 
semantics and the Curry-Howard correspondence. More precisely, we
will  see how reverse differentiation and Dialectica can be expressed in
proof  theory, lambda-calculus, and category theory.

https://pantheonsorbonne.zoom.us/j/97514275593?pwd=aXhKTTh4MWxOTkhybmJWRUtJMDFmUT09

ID réunion : 975 1427 5593
Code d’accès : 767323