GdT Sémantique des Calculs Classiques

À venir

Déjà passés

• Jeudi 21 Mars, 15h30 - 16h30, salle 1007 (Sophie Germain)
  
  Jean Louis Krivine,
  Sur les modèles de réalisabilité classique. Partie III
  
  
  
  
  
  

• Jeudi 14 Mars, 15h30 - 16h30, salle 1007 (Sophie Germain)
  
  Jean Louis Krivine,
  Sur les modèles de réalisabilité classique. Partie II
  
  
  
  
  
  

• Jeudi 7 Mars, 15h30 - 16h30, salle 1007 (Sophie Germain)
  
  Jean Louis Krivine,
  Sur les modèles de réalisabilité classique. Partie I
  Il s'agit d'une suite d'exposés sur ce sujet. On donnera les définitions de base (algèbre de réalisabilité, etc.) et on construira les modèles de ZF associés.
  On donnera diverses méthodes pour obtenir l'axiome du choix dépendant (instruction de hachage, destruction de cardinal).
  On étudiera plusieurs cas particuliers intéressants (modèles à deux ou une infinité de "threads", extensions par forcing) qui donnent des résultats de cohérence relative dans ZF avec des propriétés étranges pour R.
  
  
  
  
  
  

• Mardi 27 Novembre, 15h - 16h, salle 7D01 (Chevaleret)
  
  Pierre-Louis Curien,
  De la logique classique (polarisée) à la logique linéaire
  On détaillera un losange de traductions menant de l'une à l'autre, l'idée étant de contraindre les règles structurelles sur les positifs, puis sur les négatifs, ou vice et versa. On discutera aussi de ce que cela veut dire au niveau des constructions modèles (qui cheminent en sens inverse!).
  transparents provisoirs, à noté qu'il s'agit d'une nouvelle version de l'exposé "System L syntax for sequent calculi"
  
  
  
  
  
  

• Mardi 13 Novembre, 15h - 16h, salle 3E93 (Chevaleret)
  
  Guillaume Munch,
  Une interprétation calculatoire de la négation involutive
  Le call/cc des machines de Krivine fait correspondre au raisonnement classique des programmes qui semblent parfois inutilement compliqués. Par exemple les programmes qui correspondent à la preuve par contraposée: leur sens est obscur alors qu'on attend une explication simple.
  La raison en est qu'une pile (π) capturée par un opérateur est un objet plus primitif qu'une continuation (k_π). La machine de Krivine avec call/cc identifie les piles capturées et les continuations, ce qui entraîne la perte d'un certain nombre d'isomorphismes canoniques de la logique classique.
  On retrouve certains isomorphismes en décomposant call/cc à travers des mécanismes plus fins, qui permettent de faire la distinction entre les types de piles capturées et de continuations. (Cette distinction existe et est utile par exemple en Smalltalk.)
  Les modèles non dégénérés d'un tel calcul exhibent un phénomène "de Blass" : on ne retrouve pas toutes les lois d'associativité de la composition catégorique. L'existence de tels modèles nous amène à considérer une structure qui caractérise ce phénomène.
  (J'hérite dans tout cela de travaux de J.-Y. Girard, de C. Murthy et de V. Danos et al.)
  
  
  
  
  
  

• Mardi 16 Octobre, 15h - 16h, salle 3E91 (Chevaleret)
  
  Thomas Ehrhard
  Sémantique catégorique de lambda-mu à la LL