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
15
Mai
Séminaire Chocola
Daniel Gratzer, Elies Harington, Hiroshi Unno
Voir https://chocola.ens-lyon.fr/events/meeting-2025-05-15/
Événements passés
10
Jan
Non idempotent typing, upper bounds and exact length in the lambda and in the lambda-mu-calculus
Pierre Vial
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
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
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
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
On montrera comment interpréter μLL - la logique linéaire propositionnelle avec plus petits (μ) et plus grands (ν) points fixes de types - dans les [...]
Revisiting Call-by-value Bohm trees in light of their Taylor expansion
Giulio Manzonetto
The call-by-value lambda calculus can be endowed with permutation rules, arising from linear logic proof-nets, having the advantage of unblocking some redexes that otherwise get [...]
Évaluation sémantique en logique linéaire élémentaire
Tito Nguyen
Après avoir passé en revue l'utilisation des techniques d'évaluation sémantique pour caractériser des classes de complexité en lambda-calcul simplement typé (en particulier les travaux de [...]
The algebraic structure of classical realizability models
Etienne Miquey
Implicative algebras, developed by Alexandre Miquel, are very simple algebraic structures generalizing at the same time complete Boolean algebras and Krivine realizability algebras, in such [...]
