Au cours de la seconde moitié du siècle dernier, les mathématiques constructives ont fait d’importants progrès significatifs grâce aux interprétations calculatoires de la logique apportées par les travaux de Curry et Howard.
Alors que la correspondance entre preuves et programmes semblait initialement limitée à la logique intuitionniste et aux langages de programmation purement fonctionnel, suite à la découverte par Griffin que la logique classique pouvait être interprétée calculatoirement au moyen d’opérateurs de contrôle, de nombreux travaux en réalisabilité ont montré que l’ajout d’axiomes à un système logique correspondait à l’ajout de primitives à un langage de programmation. En particulier, l’étude du pendant calculatoire d’un axiome donnée ou des conséquences logiques d’extension de la correspondance de Curry-Howard à des calculs avec effets s’est avérée particulièrement fructueuse.

L’objectif de ce workshop est de réunir des chercheur.ses intéressé.es par ces questions, dont les travaux tournent autour des mathématiques constructives, de l’étude du contenu calculatoire des preuves et en particulier de la réalisabilité, ou dont la recherche implique des applications de la réalisabilité. Ici, le terme ”réalisabilité” est donc à prendre dans un sens très large, dans le but de favoriser les échanges entres des personnes travaillant sur ses différents aspects.