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
Revisiting Call-by-value Bohm trees in light of their Taylor expansion
Giulio Manzonetto (LIPN, Université Paris 13)
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 [...]
Une application de l’élimination parallèle des coupures en logique linéaire multiplicative sans unités au développement de Taylor des réseaux de preuves
Jules Chouquet (IRIF, Université de Paris)
TBA
Évaluation sémantique en logique linéaire élémentaire
Tito Nguyen (LIPN, Université Paris 13)
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 (IRIF, Université de Paris)
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 [...]
Extensional and intensional semantic universes: a denotational model of dependent types
Valentin Blot (IRIF, Université de Paris)
We describe a dependent type theory, and a denotational model for it, that incorporates both intensional and extensional semantic universes. In the former, terms and [...]
28
Juin
21
Juin
Higher dimensional rewriting and cubical categories
Maxime Lucas (I2M, Aix-Marseille Université)
TBA
The true concurrency of Herbrand's theorem
Pierre Clairambault (LIP, CNRS, ENS Lyon)
Herbrand's theorem, widely regarded as a cornerstone of proof theory, exposes some of the constructive content of classical logic. In its simplest form, it reduces [...]
Representing permutations without permutations, or the expressive power of sequence types
Pierre Vial (IRIF, Université de Paris)
An intersection type system with given features (strict or not, idempotent or not, relevant or not, rigid or not...) characterizing, e.g., a notion of normalization [...]
Petites catégories comme modèles des types d'homotopie
Andrea Gagna (I2M, Aix-Marseille Université)
La théorie de l'homotopie des petites catégories a été introduite par Grothendieck avec la définition du foncteur nerf, qui permet de donner une notion sensible [...]
