Réalisabilité à Chambéry, du 10 au 13 juin 2008
Quand Alexandre m'a dit « j'aimerais bien faire un cours de réalisabilité », je n'ai pas été long à réagir... Donc, pour votre bonheur à tous, nous allons avoir droit à 4 jours de réalisabilité dans un coin fort sympathique : au Bourget du Lac (juste à coté de Chambéry).
Le cours, tels que décrit par Alexandre : un des buts du cours, c'est précisément de mettre celles et ceux qui le suivent au niveau des questions qu'on abordera au groupe de travail. Donc la réponse est: le groupe de travail s'adresse effectivement « aux gens qui font de la réalisabilité toute la journée », ce qui inclura naturellement les gens qui auront assisté au cours, puisque ceux-ci auront « fait de la réalisabilité toute la journée » au moins pendant 2 jours. - Alexandre
Cette page est assez incomplète, mais j'essaierais de la tenir à jour...
Cours de réalisabilité, par Alexandre Miquel
Contenu
Pas de programme très précis, si ce n'est que le cours est destiné aux débutants plus qu'aux vétérans de la réalisabilité. (Voir plus haut.) Bien entendu, les vétérans sont les bienvenus... Voila juste ce qu'Alexandre m'a dit : Réalisabilité à la Krivine, extension à ZF et au calcul des constructions, extraction de programmes, axiome du choix, etc.
Emploi du temps
Le cours commencera le mardi 10 juin à 10h15 dans une salle encore indéterminée. (Rendez-vous dans la salle café du LAMA à partir de 9h30...)
- séance 1 : mardi 10h15--12h15, amphithéâtre « Revard »
- séance 2 : mardi 14h--16h++ (extensible au besoin), amphithéâtre « Revard »
- séance 3 : mercredi 10h15--12h15, amphithéâtre « Nivolet »
- séance 4 : mercredi 14h--16h, amphithéâtre « Nivolet »
Un objectif serait de pouvoir terminer un peu plus tôt le mardi pour ceux qui ont un train à prendre ; ou bien pour pouvoir profiter de la région pour ceux qui restent. À voir...
Participants
Voici la liste des gens qui exprimé leur intérêt pour le cours. Est-ce que vous pouvez confirmer ?
- Alexandre Miquel (PPS) 2 jours
- Pierre Hyvernat (LAMA) 2 jours
- Christophe Raffalli (LAMA) 2 jours
- Tom Hirschowitz (LAMA) 2 jours
- Guillaume Theyssier (LAMA) 1 jour
- Karim Nour (LAMA) à confirmer
- Florent Hatat (LAMA/ENS Lyon) 2 jours
- Clément Fumex (LAMA/PPS) 2 jours
- Laurent Regnier (IML) 1 jour
- Lionel Vaux (IML) 2 jours
- Emmanuel Beffara (IML) 2 jours
- Etienne Duschene (IML) 2 jours
- Marc de Falco (IML) 2 jours
- Barbara Petit (PPS) 2 jours
- Thibaut Balabonski (PPS) 2 jours
- Paul Brauner (PAREO) à confirmer
- Clément Houtmann (PAREO) à confirmer
- Bruno Bernardo (TYPICAL) 2 jours
- Aloïs Brunel (ÉNS Lyon) 2 jours
- Michele Pagani (PPS) 2 jours
- Guilhem Jaber (ÉNS Lyon / IML) 2 jours
- Matthias Puech (TYPICAL) 2 jours
Groupe de travail réalisabilité
Programme provisoire
C'est pas encore très clair, mais il devrait y avoir :
- séance 1 :, jeudi 10h15--12h30, salle de séminaires du LAMA :
- un exposé de Jean-Louis Krivine : Les formules Pi-1-1 vraies sont réalisées
- un exposé de Yves Legrandgérard : protocoles et formules valides
- séance 2 :, jeudi 14h--16h30, amphithéâtre « 4-Cantons-63 » :
- un exposé de Mauricio Guillermo (vendredi après-midi)
- un exposé de Philippe Hesse : (vendredi après-midi)
Résumé : Le but de cet exposé est d'expliquer comment réaliser un cas particulier du théorème de Herbrand (on se limite à l'élimination d'un seul quantificateur universel), dans un formalisme de réalisabilité "à la Krivine". On sera amené à utiliser l'instruction qui réalise l'axiome du choix dépendant, après avoir montré qu'elle s'adapte à une expression simple du choix au premier ordre. Si le temps le permet, on essaiera ensuite d'expliquer le comportement du terme obtenu.
- séance 3, vendredi 10h-12h, dans l'amphithéâtre « Nivolet » : une séance « ouverte » animée par Alexandre Miquel sur les différences entre la technologie Coquand/Bezem et la technologie Krivine pour réaliser l'axiome du choix
- séance 4, vendredi 14h-16h, dans l'amphithéâtre « Nivolet » : une séance « ouverte » de discussion animée par Christophe Raffalli, TBA.
Emploi du temps
Les détails suivront, mais le cours aura lieu les jeudi et vendredi 12 et 13 juin. La première séance devrait avoir lieu dans la salle de séminaires du LAMA (premier étage, à gauche au fond) jeudi 12 juin à 10h15. Les séances suivantes seront vraisemblablement dans une autre salle...
- séance 1 : jeudi 10h15--12h30, Jean-Louis Krivine et Yves Legrandgérard (exposés)
- séance 2 : 14h--16h, Alexandre Miquel (discussion / groupe de travail)
- séance 3 : vendredi 10h--12h30, Christophe Raffalli (discussion / groupe de travail)
- séance 4 : vendredi 14h--16h, Mauricio Guillermo et Philippe Hesse (exposés)
Participants
Voici la liste des gens qui se sont fait connaître. Est-ce que vous pouvez confirmer dés que vous savez si vous venez ?
- Alexandre Miquel (PPS) 2 jours
- Jean-Louis Krivine (PPS) 2 jours ?
- Yves Legrandgérard (PPS) 2 jours ?
- Philippe Hesse (PPS) 2 jours
- Mauricio Guillermo (PPS) à confirmer
- Pierre Hyvernat (LAMA) 2 jours
- Christophe Raffalli (LAMA) 2 jours
- Tom Hirschowitz (LAMA) ???
- Clément Fumex (LAMA/PPS) 2 jours
- Laurent Regnier (IML) 2 jours
- Lionel Vaux (IML) 1 jour ???
- Emmanuel Beffara (IML) 1 jour
- Marc de Falco (IML) ???
- Barbara Petit (PPS) 2 jours
- Pierre Clairambault (PPS) 2 jours
- Paul Brauner (PAREO) à confirmer
- Clément Houtmann (PAREO) à confirmer
- Bruno Bernardo (TYPICAL) 2 jours
- Aloïs Brunel (ÉNS Lyon) 2 jours
- Paul Rozière (PPS) 2 jours
Détails techniques
Venir au LAMA
Y'a déjà des gens qui ont fait une page qui explique comment venir au LAMA. Allez la voir pour plus de détails.
Une fois sur place, mon bureau est le bureau 22 (rez de chaussé, au fond du couloir à gauche) et celui de Christophe Raffalli est le bureau 23 (juste à coté du mien). Le numéro de mon bureau est le 04 79 75 94 22.
Logement
J'y connais pas grand chose, mais il y a plusieurs hôtels dans le centre de Chambéry, ou un hôtel plus proche du Lac du Bourget. Je demande des détails à Christophe...
Autres activités prévues
Suivant la densité du programme, on pourra essayer d'organiser une petite ballade une après-midi ; sinon, on proposera une sortie restaurant un soir. Bref, on trouvera des trucs à faire, même si je sais pas encore ce que ça sera...
