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
25
Sep
Linearization via Rewriting
Federico Olimpieri (LIS, Aix-Marseille)
We introduce the structural resource λ-calculus, a new formalism inwhich strongly normalizing terms of the λ-calculus can naturally berepresented, and at the same time any [...]
26
Juin
Séminaire Chocola à Lyon
Choudhury, Marshall, Pimentel (...)
Voir: https://chocola.ens-lyon.fr/events/meeting-2025-06-26.
19
Juin
∞-categorical models of linear logic
Elies Harington (LIX & LIPN)
The notion of categorical model of linear logic is now well studied and established around the notion of linear-non-linear adjunction, which encompasses the previous notions [...]
05
Juin
Getting thin spans in order
Victor Blanchi (LIS, Aix-Marseille)
Recently, Clairambault and Forest introduced the cartesian closed bicategory of thin spans of groupoids. It is a proof-relevant denotational model, akin to Fiore et al's [...]
15
Mai
Séminaire Chocola
Daniel Gratzer, Elies Harington, Hiroshi Unno (ÉNS Lyon)
Voir https://chocola.ens-lyon.fr/events/meeting-2025-05-15/
24
Avr
De la logique catégorique à la complexité descriptive catégorique [LSC]
Baptiste Chanus (LIPN, Sorbonne Paris Nord)
La catégorie syntaxique est une construction qui permet de raisonner sur la logique à l'aide des outils de la théorie des catégories. D'un autre côté, [...]
17
Avr
Double indexed differential linear logic reconciling resources and differential operators
Simon Mirwasser (LIPN, Sorbonne Paris Nord)
Graded Linear Logic is a central development of Linear Logic, quantifying the use of resources in proofs and programs. Differential Linear Logic, on the other [...]
01
Avr
Combinatorial proofs for classical and intuitionistic logic [Lirica]
Lutz Straßburger (LIX, INRIA Saclay)
(Séminaire de l’équipe Lirica au LIS) Combinatorial proofs, or “proofs without syntax”, form a graphical semantics of proof in various logics that is canonical yet [...]
27
Mar
Monotone weak distributive laws in categories of algebras [LSC]
Quentin Aristote (IRIF, Paris Cité)
Within the study of the semantics of programming languages, computational effects may be modelled with monads, and weak distributive laws between monads are then a [...]
20
Mar
The E-base of finite semidistributive closure lattices [LSC]
Simon Vilmin (LIS, Aix-Marseille)
A (finite) closure space is a pair consisting of a (finite) ground set X and a closure operator on X. When ordered by inclusion, the [...]
