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
Caractérisation des comportements de la Ludique
Myriam Quatrini (I2M, Aix-Marseille Université)
J.-Y. Girard a développé, au début des années 2000, une théorie logique : la Ludique, dans laquelle l’interaction est la notion primitive. En collaboration avec [...]
dPAω: a dependently-typed classical arithmetic in finite types which proves dependent choices
Hugo Herbelin (INRIA, Rocquencourt-Paris)
We extend classical arithmetic in finite types with an intuitionistically-restricted form of strong projection of existential quantification. In this system, by turning countable universal quantification [...]
Open Call-by-Value
Giulio Guerrieri (PPS, Université Paris-Diderot)
The elegant theory of the call-by-value lambda-calculus relies on weak evaluation and closed terms, that are natural hypotheses in the study of programming languages. To [...]
Logics for Weighted Automata and Transducers
Benjamin Monmege (LIF, Aix-Marseille Université)
SÉMINAIRE COMMUN I2M (LDP) - LIF (MOVE) This talk will present some of the recent results obtained in the community on the relationship between weighted [...]
Vers un compilateur prouvé d'Esterel vers les circuits
Lionel Rieg (ENS Lyon)
Les langages synchrones sont une famille de langage de programmation dédiés aux programmes temps-réel, c'est à dire avec des contraintes fortes de réactivité. Dans cette [...]
Diagrammes de cordes pour la représentation des réseaux de preuves
Matteo Acclavio (I2M, Aix-Marseille Université)
TBA
Le modèle relationnel est injectif pour MELL
Daniel de Carvalho (Innopolis University, Republic of Tatarstan, Russie)
On montre que la sémantique relationnelle est injective pour le fragment multiplicatif exponentiel des réseaux de preuve de la logique linéaire, c'est-à-dire que l'égalité entre [...]
Typed realizability for first-order classical analysis
Valentin Blot (University of Bath)
We describe a realizability framework for classical first-order logic in which realizers live in (a model of) typed lambda-mu-calculus. This allows a direct interpretation of [...]
Fixed-point elimination in the Intuitionisitic Propositional Calculus
Luigi Santocanale (LIF, Aix-Marseille Université)
It is a consequence of existing literature that least and greatest fixed-points of monotone polynomials on Heyting algebras—that is, the algebraic models of the Intuitionistic [...]
Réécriture linéaire et théorème de Squier pour les algèbres
Yves Guiraud (PPS, Université Paris-Diderot)
À la fin des années 1980, Craig Squier a résolu une conjecture portant sur la possibilité ou non, pour un monoïde de type fini ayant [...]
