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
07
Mar
Combinatoire de l’élimination des coupures de MLL, et une application au développement de Taylor de MELL
Lionel Vaux Auclair (I2M, Aix-Marseille Université)
TBA (travail en collaboration avec Jules Chouquet)
Lambda Calculus and Probabilistic Computation
Claudia Faggian (IRIF, Université de Paris)
In order to model higher-order probabilistic computation, a natural approach is to take the lambda calculus as a paradigm, and to enrich it with an [...]
Un modèle de réalisabilité pour une version faible de l'axiome du choix (∀α.AC_α)
Laura Fontanella, Guillaume Geoffroy (I2M, Aix-Marseille Université)
TBA Laura FONTANELLA Guillaume GEOFFROY
17
Jan
Towards a Proof Theory of the Riesz Modal Logic
Christophe Lucas (LIP, ENS Lyon)
It has recently been shown that two Riesz-modal-logic formulas are semantically equivalent if and only if they are equivalent when interpreted in all "modal Riesz [...]
10
Jan
Non idempotent typing, upper bounds and exact length in the lambda and in the lambda-mu-calculus
Pierre Vial (IRIF, Université de Paris)
Non-idempotent intersection type theory, introduced independently by Gardner [94], Kfoury [96] and de Carvalho [07] arguably give the simplest to prove characterizations of semantical properties [...]
Matroïdes et leur graphes des bases
Victor Chepoi (LIS, ARCO team, Aix-Marseille Université)
En première partie de l'exposé nous présentons une introduction aux matroïdes et leur définition axiomatique : libres, bases, circuits, fonction de rang, fermeture, dualité, algo [...]
Linear Implicative Algebras, towards a BHK interpretation of linear logic
Luc Pellissier (LIP, ENS Lyon)
Implicative Algebras were recently introduced as a unified framework for forcing and realisability, whose particularity is to interpret terms and formulæ uniformly. - In this [...]
22
Nov
Connecting models of differential linear logic with reloids
Zeinab Galal (IRIF, Université de Paris)
Species of structures were introduced by Joyal as a unified framework for the theory of generating series in enumerative combinatorics. Species are connected to Girard's [...]
Sémantique dénotationnelle de la logique linéaire avec plus petits et plus grands points fixes de types
Thomas Ehrhard (IRIF, Université de Paris)
On montrera comment interpréter μLL - la logique linéaire propositionnelle avec plus petits (μ) et plus grands (ν) points fixes de types - dans les [...]
