|
|
 |
Lieu et horaires:
- bâtiment A33 (présidence/maths) étage 2 salle 2 (plan du campus Bx1)
- attention changement d'horaire: les mercredis de 11:00 à 12:00
Objectifs
Cette petite école est destinée aux collègues et aux doctorants en informatique ou en mathématiques (ces derniers pourront comptabiliser ces heures dans le cadre de leur formation doctorale). Elle demandera un peu d'indulgence aux participants car les intervenants ne maîtrisent pas d'avance l'ensemble des sujets qu'ils vont pourtant tenter de présenter.
Il s'agit en premier lieu de découvrir les modèles mathématiquement naturels de la logique intuitionniste construits sur les notions de faisceau et de topos. Initiée par Grothendieck dans le cadre de la géométrie algébrique, l'étude logique des topoi a été principalement poursuivie, dans le sillage de Lawvere, par des catégoriciens. A ce titre, notre école devrait déboucher sur quelques questions ouvertes, comme la définition de modèles complets pour la logique linéaire du premier ordre (avec des applications prometteuses au typage sémantique en linguistique formelle comme à la spécification de programmes). Pour reprendre la terminologie de Jean-Yves Girard, il s'agit là du niveau (-1) des fondations. Il a déjà bien été exploré en l'an dernier, même si on y reviendra.
L'étude de la sémantique catégorique des preuves, beaucoup utilisé poru la sémantique des langages de programmation fonctionnels typés, soit le niveau (-2) sera elle aussi étudié. La dynamique des preuves (le niveau -3) sera aussi étudiée, qu'elle se place dans le cadre ludique ou dans celui des algèbres d'opérateurs. Le lien entre ces niveaux nous intéressera tout particulièrement.
Les applications envisagées, sans exclure celles à la sémantique dela programmation, se situeront plutôt en philosophie du langage et en linguistique: sémantique de la phrase, du discours ou du dialogue, sémantique lexicale.
Documents:
Séances:
- Année précédente: voir ici.
- vendredi 24 septembre 2010 Michele Absrusci (INRIA / Roma tre)
Introduction à la logique linéaire.
- vendredi 1er octobre 2010 (ChR)
espaces cohérents et connecteurs linéaires
- vendredi 8 octobre 2010 (ChR)
des preuves aux réseaux de preuves
correction syntaxique et sémantique des réseaux
- vendredi 15 octobre (ChR)
des réseaux aux preuves
- vendredi 22 octobre (ChR)
correction et interprétation sémantique
- vendredi 29 octobre: relâche
- vendredi 5 novembre (ChR)
normalisation (un pas vers la géométrie de l'interaction)
- Vendredi 12 et samedi 13 novembre colloque
Logique, catégories, sémantique
- vendredi 19 novembre relâche
- vendredi 26 novembre relâche
- vendredi 3 décembre Michele Abrusci
de la logique linéaire à la ludique: polarité, focalisation et lieux
- longue pause et changement d'horaire:
à compter du 2 mars l'école a lieu les mercredis de 11 à 12
- mercredi 2 mars Boas Erez
logique spéculaire (d'après René Guitart)
- relâche le mercredi 9 mars
- mercredi 16 mars Boas Erez
logique spéculaire (d'après René Guitart)suite
- relâche le mercredi 23 mars
- mercredi 30 mars Ivano Ciardelli
préfaisceaux de modèles pour la complétude
de la logique intuitionnsite du premier ordre
- mercredi 6 avril Ivano Ciardelli
préfaisceaux de modèles pour la complétude
de la logique intuitionnsite du premier ordre - suite
- mercredi 6 avril Ivano Ciardelli
préfaisceaux de modèles pour la complétude
de la logique intuitionnsite du premier ordre - fin
- vacances de printemps
- mercredi 4 mai Ophélie Lacroix
modèles de la logique classique du second ordre
|
Bibliographie:
- Pierre CARTIER, Logique, catégories et faisceaux. Séminaire Bourbaki, 20 (1977-1978), Exp. No. 513, 24 p.
- Jean-Yves GIRARD Le point aveugle — cours de logique Volumes I & II, Hermann, 2006.
- Peter T JOHNSTONE Sketches of an Elephant: A Topos Theory Compendium, Volumes I & II Oxford Logic Guides (vol. 43 & 44), Oxford University Press, 2003.
- Joachim LAMBEK & Phil SCOTT Introduction to Higher-Order Categorical Logic Cambridge studies in advanced mathematics Cambridge University Press, 1988
- Saunders MAC LANE & Ieke MOERDIJK Sheaves in geometry and logic: a first introduction to topos theory Springer University Texts, 1993
- Anne Sjerp TROELSTRA & Dirk VAN DALEN Constructivism in mathematics, Vol I & II, North-Holland, 1988.
|
| |
|
