Organizing Committee
Comité d’organisation
Étienne Miquey (Aix-Marseille Université)
During the second half of the last century, constructive mathematics made significant progress thanks to the computational interpretations of logic brought by Curry and Howard’s work.
While the proofs-as-programs correspondence seemed for a time to be bounded to intuitionistic logic and purely functional programming language, following Griffin’s computational interpretation of classical logic through control operators, advances in realizability during the last decades have shown that adding axioms to a logical system corresponds to adding computing primitives to a programming language. In particular, studying the computational counterpart of a given axiom or the logical consequences of effectful extensions of the proof asprograms paradigm have shown to be particularly fruitful.
The goal of this workshop is to bring together researchers interested in these questions, whose work revolve around constructive mathematics, the study of the computational content of proofs, and in particular in realizability or whose research involves applications of realizability. Here, “realizability” is thus to be understood in a very broad sense to foster new ideas from interaction of people working on its different aspects.
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.
SPEAKERS
To be announced
SPONSOR
