Localisation

Adresses

Aix-Marseille Université
Institut de Mathématiques de Marseille (I2M) - UMR 7373
Site Saint-Charles : 3 place Victor Hugo, Case 19, 13331 Marseille Cedex 3
Site Luminy : Campus de Luminy - Case 907 - 13288 Marseille Cedex 9

Responsable
Fréquence

hebdomadaire (sauf conflit avec Chocola)

Jour-Horaires

Jeudi. 11h-12h30

Lieu

Luminy (accès), salle de séminaire (304-306)

 

Contacts

lionel.vaux_at_univ-amu.fr

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

30 Apr

Séminaire Chocola à Lyon

Castellan, TBA, TBA (ÉNS Lyon)

Voir le site de Chocola.
07 May

TBA

Ralph Sarkis (University College London)

21 May

TBA

Adrienne Lancelot (Università di Bologna)

28 May

Séminaire Chocola à Lyon

van Gool, TBA, TBA (ÉNS Lyon)

Voir le site.

Événements passés

Fibrations of Tree Automata

Fibrations of Tree Automata

Colin Riba (LIP, ENS Lyon)

15/10/2015    
11h00 - 12h00
We propose a notion of morphism between tree automata based on game semantics. These morphisms are winning strategies on a synchronous restriction of the linear [...]
Utilisation de catégories supérieures pour les résolutions d'algèbres

Utilisation de catégories supérieures pour les résolutions d'algèbres

Eric Hoffbeck (LAGA, Université Paris 13)

08/10/2015    
11h00 - 12h00
Des propriétés homologiques des monoïdes peuvent être prouvées grâce aux polygraphes (des catégories supérieures, construites inductivement, dont le but est d'encoder la géométrie des relations [...]
L'instruction fork et le principe d'induction en réalisabilité  classique

L'instruction fork et le principe d'induction en réalisabilité classique

Guillaume Geoffroy (I2M, Aix-Marseille Université)

24/09/2015    
11h00 - 12h00
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

Calcul oriental

Yves Lafont (I2M, Aix-Marseille Université)

09/07/2015    
14h00 - 15h00
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

Realizability games for the specification problem

Etienne Miquey (PPS, Université Paris-Diderot)

02/07/2015    
11h00 - 12h00
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

Un résultat de full-abstraction pour les arbres de Böhm du lambda-calcul probabiliste

Thomas Leventis (I2M, Aix-Marseille Université)

25/06/2015    
11h00 - 12h00
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

Interacting Hopf algebras: the string diagrammatic theory of linear subspaces

Fabio Zanasi (University College London)

18/06/2015    
11h00 - 12h00
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

Vers l'unification des systèmes de types pour processus mobiles

Emmanuel Beffara (I2M, Aix-Marseille Université)

04/06/2015    
11h00 - 12h00
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 May

Treillis et extensions de la logique linéaire additive

Olivier Laurent (LIP, CNRS, ENS Lyon)

28/05/2015    
11h00 - 12h00
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

Représentation des fonctions continues entre "streams" (& Co.) par des types de données

Pierre Hyvernat (LAMA, Université Savoie Mont Blanc)

23/04/2015    
11h00 - 12h00
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é [...]
19 20 21 22 23 24 25 26
Secured By miniOrange