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
26
Oct
Graphical Languages for Quantum Computation
Marc de Visme (INRIA Paris-Saclay)
In this talk, we will go through the basics of graphical languages for quantum computation, their advantages and uses, and the two main traditions of [...]
19
Oct
12
Oct
From Thin Concurrent Games to Relational Models
Pierre Clairambault (LIS)
Denotational models can roughly be classified in two kinds: static models (domains, relations, coherence spaces, etc), which record atemporal final "states" of completed executions; and [...]
05
Oct
Dans les réseaux de démonstration, on peut sauter à l’élastique en toute sécurité (et c’est la preuve de séquentialisation du LLHandbook)
Lionel Vaux-Auclair (I2M)
Dans un cours d’introduction à la logique linéaire, si on parle de réseaux, on énonce généralement un résultat de séquentialisation : tout réseau est la [...]
28
Sep
Séminaire Chocola à Lyon
(...)
Voir https://chocola.ens-lyon.fr/events/meeting-2023-09-28/. Le matin en salle 435 (4ème étage -- à confirmer), et l'après-midi en amphi B. Ces deux salles sont sur le site [...]
21
Sep
La bicatégorie cartésienne close des spans fins
Simon Forest (LIS)
Dans le modèle Rel de la logique linéaire, les types sont interprétés par des ensembles, et les preuves/programmes par des relations. Une idée naturelle pour [...]
14
Sep
Deux définitions alternatives des ω-catégories (et leurs généralisations homotopiques)
Félix Loubaton (Labo J. Dieudonné, Nice)
Nous donnerons deux définitions alternatives des ω-catégories. La première repose sur la catégorie Θ de Joyal et la deuxième sur le nerf de Street et [...]
29
Juin
Concurrent Realizability on Conjunctive Structures
Étienne Miquey (I2M)
This work aims at exploring the algebraic structure of concurrent processes and their behavior independently of a particular formalism used to define them. We propose [...]
29
Juin
Strategies as Resource Terms, and their Categorical Semantics
Lison Blondeau-Patissier (I2M & LIS)
As shown by Tsukada and Ong, normal (extensional) simply-typed resource terms correspond to playsin Hyland-Ong games, quotiented by Melliès’ homotopy equivalence. Though inspiring, their proofis [...]
22
Juin
Simply typed β-convertibility is TOWER-complete even for safe λ-terms
Lê Thành Dũng (Tito) Nguyễn (ENS Lyon)
We consider the following decision problem: given two simply typed λ-terms, are they β-convertible? Equivalently, do they have the same normal form? It is famously [...]
