Organizing Committee
Comité d’organisation
Étienne Miquey (Aix-Marseille Université)
IMPORTANT WARNING: Scam / Phishing / SMiShing ! Note that ill-intentioned people may be trying to contact some of participants by email or phone to get money and personal details, by pretending to be part of the staff of our conference center (CIRM). CIRM and the organizers will NEVER contact you by phone on this issue and will NEVER ask you to pay for accommodation/ board / possible registration fee in advance. Any due payment will be taken onsite at CIRM during your stay.
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
SPONSORS
