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
16
Sep
Injectivité positionnelle pour les stratégies innocentes
Lison Blondeau-Patissier (I2M, Aix-Marseille)
Melliès a montré que les stratégies innocentes étaient positionnelles dans les jeux asynchrones : leur comportement dépend de la position, et pas de l'ordre temporel [...]
Coherent differentiation
Thomas Ehrhard (IRIF, Université de Paris)
The categorical models of the differential lambda-calculus are additive categories because of the Leibniz rule which requires the summation of two expressions. This means that, [...]
Sémantiques relationnelles et traductions modales pour Generalized Basic Logic
Wesley Fussner (Laboratoire Dieudonné, Université Côte d'Azur)
« Generalized Basic Logic » est une logique sous-structurelle située à l'intersection de la « Basic Logic » de Hájek et de la logique intuitionniste [...]
The concurrent games abstract machine
Pierre Clairambault (LIP, ÉNS Lyon)
In this talk, I will introduce the concurrent games abstract machine: a multi-token machine for Idealized Parallel Algol (IPA), a higher-order concurrent programming language with [...]
Gluing resource proof-structures: inhabitation and inverting the Taylor expansion
Giulio Guerrieri (University of Bath, UK)
A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing those [...]
Compositional relational reasoning via operational game semantics
Guilhem Jaber (LS2N, Nantes)
We use operational game models as a guide to develop relational techniques for establishing contextual equivalences with respect to contexts drawn from a hierarchy of [...]
Spécification mathématique de langages de programmation via les monades et leurs modules
Ambroise Lafont (Data61, CSIRO, Cogent team, Sydney)
La recherche dans le domaine des langages de programmation s'appuie traditionnellement sur une définition de syntaxe modulo renommage des variables liées, avec la sémantique opérationnelle [...]
Evidenced frames: a unifying framework broadening realizability models
Étienne Miquey (LIP, ÉNS Lyon)
Constructive foundations have for decades been built upon realizability models for higher-order logic and type theory. However, traditional realizability models have a rather limited notion [...]
Gluing resource proof-structures: inhabitation and inverting the Taylor expansion
Giulio Guerrieri (University of Bath, UK)
A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing those [...]
Une extension du cadre de Batanin pour les catégories supérieures
Simon Forest (LIX, École polytechnique, Palaiseau)
Les catégories supérieures sont une généralisation des catégories usuelles où l'on a non seulement des cellules en dimension 0 et 1 (des objets et des [...]
