Séminaire Logique et Interactions
Le séminaire Logique et Interaction est le séminaire de l’équipe LDP de l’I2M. Il est conjoint au séminaire de l’équipe LSC du LIS.
Une liste de diffusion (modérée) pour recevoir les annonces d’exposés : i2m-seminaire-logique@univ-amu.fr
Pour s’inscrire, contacter le responsable.
Les prochains séminaires
18
Déc
Événements passés
L'instruction fork et le principe d'induction en réalisabilité classique
Guillaume Geoffroy (I2M, Aix-Marseille Université)
Je commencerai par quelques rappels sur les modèles de réalisabilité classique de l'arithmétique d'ordre 2, puis je montrerai le lien entre l'instruction « fork » [...]
Calcul oriental
Yves Lafont (I2M, Aix-Marseille Université)
L’oriental de dimension n est le simplexe de dimension n muni d’une structure de n-catégorie (stricte). Il est donc orienté en un sens assez fort [...]
Realizability games for the specification problem
Etienne Miquey (PPS, Université Paris-Diderot)
In Krivine classical realizability, one can understand the truth value of a formula (that is the set of its realizers) as its defenders, and the [...]
Un résultat de full-abstraction pour les arbres de Böhm du lambda-calcul probabiliste
Thomas Leventis (I2M, Aix-Marseille Université)
L'étude du lambda-calcul probabiliste est habituellement restreinte à des stratégies de réductions limitées. Notre objectif est d'étudier le calcul obtenu en ôtant toute contrainte sur [...]
Interacting Hopf algebras: the string diagrammatic theory of linear subspaces
Fabio Zanasi (University College London)
We introduce the theory IH of interacting Hopf algebras, parametrised over a principal ideal domain R. The axioms of IH are derived using Lack’s approach [...]
Vers l'unification des systèmes de types pour processus mobiles
Emmanuel Beffara (I2M, Aix-Marseille Université)
Ce travail présente un cadre unificateur pour les systèmes de types pour les algèbres de processus. Le cœur du système fournit une correspondance précise entre [...]
28
Mai
Treillis et extensions de la logique linéaire additive
Olivier Laurent (LIP, CNRS, ENS Lyon)
Certaines structures ordonnées libres peuvent être représentées à l'aide de la relation de déduction du calcul des séquents. En particulier, Withman a montré par anticipation [...]
Représentation des fonctions continues entre "streams" (& Co.) par des types de données
Pierre Hyvernat (LAMA, Université Savoie Mont Blanc)
Brouwer savait déjà que les fonctions continues entre streams (avec la topologie produit habituelle) pouvaient être représentées par des arbres infinis. Peter Hancock a montré [...]
Bar recursion, sémantique dénotationnelle et réalisabilité classique
Jean-Louis Krivine (PPS, Université Paris-Diderot)
L'opérateur de bar recursion, introduit dans les années 60 par C. Spector pour "prouver" la consistance de l'Analyse, a été recyclé à partir de 1998, [...]
Types inductifs stricts et paresseux, du point de vue de la logique linéaire
Thomas Ehrhard (PPS, Université Paris-Diderot)
TBA http://www.pps.univ-paris-diderot.fr/~ehrhard/
