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

etienne.miquey_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

25 Jun

Séminaire Chocola à Lyon

Gavazzo, Lancelot, TBA (LIP, ENS Lyon)

02 Jul

Événements passés

La théorie des ensembles cinquante ans après Cohen

La théorie des ensembles cinquante ans après Cohen

Patrick Dehornoy (LMNO, Université de Caen)

28/09/2017    
11h00 - 12h00
On présentera quelques résultats de théorie des ensembles récents, avec un accent sur l'hypothèse du continu et la possibilité de résoudre la question après les [...]
Two type-theoretic approaches to probabilistic termination

Two type-theoretic approaches to probabilistic termination

Charles Grellois (INRIA Sophia-Antipolis )

21/09/2017    
11h00 - 12h00
A fundamental result in lambda-calculus states that terms that admit a simple type are strongly normalizing: in other words, they always terminate. The simply-typed lambda-calculus [...]
Un contre-exemple à la conjecture de Thiagarajan sur les structures d'évènements régulières

Un contre-exemple à la conjecture de Thiagarajan sur les structures d'évènements régulières

Victor Chepoi (LIF, Aix-Marseille Université)

22/06/2017    
11h00 - 12h00
On présente un contre-exemple à la conjecture de Thiagarajan (1996 et 2002) affirmant que les structures d'évènements régulières correspondent exactement à celles obtenues comme dépliages [...]
Linear approximations, fibrations, intersection types

Linear approximations, fibrations, intersection types

Luc Pellissier (LIPN, Université Paris 13)

15/06/2017    
11h00 - 12h00
We investigate intersection types from the “type systems as functors” viewpoint, as recently given by Melliès and Zeilberger. After recasting type-theoretic notions such as subject [...]
Théorie homotopique des types et modèles algébriques pour les infinis catégories et groupoïdes

Théorie homotopique des types et modèles algébriques pour les infinis catégories et groupoïdes

Simon Henry (Collège de France, Paris)

30/05/2017    
14h00 - 15h30
Dans le cadre de la Journée "Autour de l’hypothèse homotopique de Grothendieck". Dans son manuscrit “À la poursuite des champs” Grothendieck propose une définition “d'infini-groupoïde” [...]
Globular models for weak higher dimensional structures

Globular models for weak higher dimensional structures

Edoardo Lanari (Macquarie University)

30/05/2017    
11h00 - 12h30
Dans le cadre de la Journée "Autour de l’hypothèse homotopique de Grothendieck". [su_spacer size="10"] The state of the art of higher category theory offers a [...]
Syntaxe et sémantique des diagrammes de preuve

Syntaxe et sémantique des diagrammes de preuve

Matteo Acclavio (LMNO, Université de Caen)

23/05/2017    
11h00 - 12h00
TBA https://www.lmno.cnrs.fr/?q=equipes/agl
04 May

Opérateurs de réduction et complétion de systèmes de réécriture linéaires

Cyrille Chenavier (IRIF, Université de Paris)

04/05/2017    
11h00 - 12h00
En réécriture, la confluence est une propriété garantissant que lorsque deux réductions sont issues d'un même terme, celles-ci confluent vers un terme commun. Dans cet [...]
Shapely monads and analytic functors

Shapely monads and analytic functors

Tom Hirschowitz (LAMA, Université Savoie Mont Blanc)

30/03/2017    
11h00 - 12h00
In this work, we give precise mathematical form to the idea of a structure whose data and axioms are faithfully represented by a graphical calculus; [...]
The complete unsoundness of coinductive intersection types (and how to escape it)

The complete unsoundness of coinductive intersection types (and how to escape it)

Pierre Vial (IRIF, Université de Paris)

23/03/2017    
11h00 - 12h00
Certain type assignment systems are known to guarantee or characterize normalization. The grammar of the types they feature is usually inductive. It is easy to [...]
Secured By miniOrange