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
20
Nov
Séminaire Chocola à Lyon
Marin, Walch, Wrigley
Détails ici : https://chocola.ens-lyon.fr/events/seminaire-2025-11-13/
27
Nov
11
Déc
Séminaire Chocola à Lyon
Cailler, Paquet, TBA
Détails ici : https://chocola.ens-lyon.fr/events/seminaire-2025-10-16/
18
Déc
Événements passés
Le modèle relationnel est injectif pour MELL
Daniel de Carvalho
On montre que la sémantique relationnelle est injective pour le fragment multiplicatif exponentiel des réseaux de preuve de la logique linéaire, c'est-à-dire que l'égalité entre [...]
Typed realizability for first-order classical analysis
Valentin Blot
We describe a realizability framework for classical first-order logic in which realizers live in (a model of) typed lambda-mu-calculus. This allows a direct interpretation of [...]
Fixed-point elimination in the Intuitionisitic Propositional Calculus
Luigi Santocanale
It is a consequence of existing literature that least and greatest fixed-points of monotone polynomials on Heyting algebras—that is, the algebraic models of the Intuitionistic [...]
Réécriture linéaire et théorème de Squier pour les algèbres
Yves Guiraud
À la fin des années 1980, Craig Squier a résolu une conjecture portant sur la possibilité ou non, pour un monoïde de type fini ayant [...]
Quillen's theorem A and categories as model for homotopy types
Andrea Gagna
Quillen proved his Theorem A in the '70s in order to have a powerful tool to investigate weak equivalences between nerves of small categories. This [...]
Fibrations of Tree Automata
Colin Riba
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
Eric Hoffbeck
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
Guillaume Geoffroy
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
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 [...]
