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
12
Fév
Is typed realizability only predicative?
Félix Castro (I2M, Aix-Marseille)
In Kleene realizability, formulas are interpreted as sets of (untyped) programs. This approach allows for a sound interpretation of Higher-Order Logic (HOL): it leads to [...]
19
Fév
Ohana trees, Taylor expansion and multi-type semantics for the λI-calculus. No variable gets left behind or forgotten!
Rémy Cerda (Università di Bologna)
The standard notion of evaluation trees for the λ-calculus, namely Böhm trees, is quite ill-behaved with respect to the inputs of programs, namely free variables: [...]
Événements passés
On higher-order cryptography - Raphaëlle Crubillé
Raphaëlle Crubillé (LORIA, PESTO team, Nancy)
Type-two constructions abound in cryptography: adversaries for encryption and authentication schemes, if active, are modeled as algorithms having access to oracles, i.e. as second-order algorithms. [...]
The Bicategory of “Open Functors” and its Friends – Luidnel Maignan
Luidnel Maignan (LACL, UPEC, Créteil)
We want to replace categories, functors and natural transformations by categories, open functors and open natural transformations. The adjective open is added here to mean [...]
A multicategorical approach to mixed linear-non-linear substitution - Christine Tasson
Christine Tasson (LIP6, Sorbonne Université)
I will present a colimit construction of 2-monad that we studied with Martin Hyland with the purpose of understanding the mixed linear-non-linear framework at play [...]
12
Nov
Un groupoïde d’arbres de permutations (suite)
(...)
La dernière fois, j’ai introduit une notion d’arbres de permutations, qui s’organisent en un groupoïde agissant sur les arbres planaires enracinés avec feuilles étiquetées, c.-à-d. [...]
08
Oct
Un groupoïde d’arbres de permutations
Lionel Vaux Auclair (I2M, Aix-Marseille Université)
J’introduirai une notion d’arbres de permutations, qui s’organisent en un groupoïde agissant sur les arbres planaires enracinés avec feuilles étiquetées, c.-à-d. les termes du premier [...]
Finding Resolution in unexpected places: Girard's formula outside its usual setting
Peter Hines (YCCSA, York, UK)
WEBINAIRE (visio: https://greenlight.lal.cloud.math.cnrs.fr/b/lio-hdc-jef) Abstract: This is not a talk about Linear Logic or the Geometry of Interaction; these feature, very briefly, as historical background & [...]
Théorie des types pour les oméga-catégories faibles
Thibaut Benjamin (LIX, École polytechnique, Palaiseau)
Les oméga-catégories faibles sont une généralisation des catégories dans lesquelle chaque catégorie possède non seulement des objets et des flèches, mais aussi des cellules de [...]
05
Déc
Un programme d'algebrisation pour la réalisabilité ? (annulé)
Mauricio Guillermo (Universidad de la República, Uruguay)
Dans cet exposé, je me propose d'introduire les motivations du programme de travail qu'on poursuit à Montevideo depuis un moment. On remonte à la lecture [...]
Homologie des infini-catégories strictes
Léonard Guetta (IRIF, Université Paris Diderot)
Dans cet exposé, je présenterai une partie des travaux que j'ai effectués au cours de ma thèse et qui s'articulent autour de la théorie de [...]
On discrete idempotent paths
Luigi Santocanale (LIS, LIRICA team, Aix-Marseille Université)
The set of discrete lattice paths from (0, 0) to (n, n) with North and East steps (i.e. words w ∈ { x, y } [...]
