|
∂ is for dialectica: when proofs and programs meet differentiation| title | ∂ is for dialectica: when proofs and programs meet differentiation |
|---|
| start_date | 2024/03/25 |
|---|
| schedule | 17h-19h |
|---|
| online | no |
|---|
| location_info | Salle des conférences de l'IHPST & sur Zoom |
|---|
| summary | Dialectica is a proof transformation acting on intuitionistic logic, 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. |
|---|
| responsibles | Pataut, Poggiolesi |
|---|
Workflow history| from state (1) | to state | comment | date |
|---|
| submitted | published | | 2024/03/20 16:38 UTC |
| |
|