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
24
Mar
Proof nets, rings, and ideals
William Troiani (LIPN, Université Sorbonne Paris Nord)
What is cut elimination? When Gentzen wrote down the rewriting processes associated with his logical systems, what seemingly external mathematical structure was he also encapsulating? [...]
17
Mar
Les jeux de gabarit, un modèle homotopique de la logique linéaire différentielle
Paul-André Melliès (IRIF, Paris Cité)
03
Mar
Automates implicites en λ-calcul typé
Lê Thành Dũng Nguyễn (IRISA, Rennes)
La correspondance preuves-programmes fait intervenir des langages de programmation totaux, qui ne sont donc pas Turing-complets. Quels prédicats ou quelles fonctions peut-on définir par des [...]
13
Jan
Sémantique des jeux pour la logique modale CK
Davide Catta (LIRMM, Montpellier)
Les logiques modales constructives sont obtenues en étendant la logique propositionnelle intuitionniste avec certains axiomes modaux. De nombreux systèmes de preuve sont connus pour ces [...]
Geometry of Interaction for ZX-Diagrams
Kostia Chardonnet (LRI, Paris-Saclay + IRIF, Université de Paris)
ZX-Calculus is a versatile graphical language for quantum computation equipped with an equational theory. Getting inspiration from Geometry of Interaction, in this work we propose [...]
09
Déc
Développement de Taylor en λ-calcul infinitaire, suite
Rémy Cerda (I2M, Aix-Marseille)
Formalisme appuyé sur la logique linéaire de Girard, le développement de Taylor de λ-termes développé par Ehrhard et Regnier a été largement utilisé comme outil [...]
25
Nov
Développement de Taylor en λ-calcul infinitaire
Rémy Cerda (I2M, Aix-Marseille)
Formalisme appuyé sur la logique linéaire de Girard, le développement de Taylor de λ-termes développé par Ehrhard et Regnier a été largement utilisé comme outil [...]
Template games: a categorical combinatorics of scheduling and synchronisation
Paul-André Melliès (IRIF, Université de Paris)
TBA
30
Sep
Une lecture technique de la syntaxe transcendantale
Boris ENG (LIPN, Paris 13)
Dans cet exposé, je présente une interprétation technique du projet de syntaxe transcendantale de Girard que j'ai réalisée avec Thomas Seiller. Ce projet esquisse un [...]
