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
28
Nov
Qu’est ce qu’un foncteur polynomial et à quoi ça sert? (2/2)
Christine Vespa (I2M, Aix-Marseille Université)
Cet exposé est une introduction à la notion de foncteur polynomial introduite par Eilenberg et MacLane dans les années 1950, comme étant une généralisation des [...]
21
Nov
14
Nov
Qu’est ce qu’un foncteur polynomial et à quoi ça sert? (1/2)
Christine Vespa (I2M, Aix-Marseille Université)
Cet exposé est une introduction à la notion de foncteur polynomial introduite par Eilenberg et MacLane dans les années 1950, comme étant une généralisation des [...]
24
Oct
Böhm and Taylor for all
Aloÿs Dufour (LIPN, Sorbonne Paris Nord)
Böhm approximations, used in the definition of Böhm trees, are a staple of the semantics of the lambda-calculus. Introduced more recently by Ehrhard and Regnier, [...]
17
Oct
10
Oct
Tropical Mathematics and The Lambda Calculus
Paolo Pistone (LIP, ÉNS Lyon)
We explore the interpretation of the lambda-calculus in a framework based on tropical mathematics, and we show that it provides a unifying framework for two [...]
03
Oct
A recipe for the semantics of reversible programming [LSC]
Louis Lemonnier (Edinburgh)
In this presentation, we explore the foundational elements required to interpret reversible programming within a categorical framework. We use the symmetric pattern-matching language introduced by [...]
26
Sep
Morphismes cartésiens en jeux concurrents
Pierre Clairambault (LIS, Aix-Marseille)
On comprend désormais bien comment relier les jeux aux modèles quantitatifs tels que le modèle relationnel: il suffit d'"oublier le temps" ou la causalité, et [...]
19
Sep
12
Sep
Automatisation des calculs dans les catégories supérieures et génération de preuves d'égalités
Thibaut Benjamin (Cambridge)
Dans cet exposé, je vais présenter une approche pour travailler avec les types d'identité supérieurs en théorie des types homotopique, s'appuyant sur un langage intermédiaire [...]
