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
29
Sep
On some toposes of topological setoids
Fabio Pasquali (IRIF, Université de Paris)
By “category topological setoids” we mean a category whose objects are pairs (A,R) where A is a topological space and R is an equivalence relation [...]
Classical realizability from relative realizability
Thomas Streicher (Technische Universität Darmstadt)
TBA
Homological computations for term rewriting systems
Samuel Mimram (LIX, Polytechnique Palaiseau)
An important problem in universal algebra consists in finding presentations of algebraic theories by generators and relations, which are as small as possible. Exhibiting lower [...]
Une sémantique des jeux parallèle pour PCF
Pierre Clairambault (LIP, CNRS, ENS Lyon)
PCF est le langage paradigmatique pour la programmation séquentielle d'ordre supérieur. Mais bien que séquentiel, étant purement fonctionnel, son ordre d'évaluation ne peut être observé [...]
Modèles de réalisabilité classique par réalisateurs universels
Guillaume Geoffroy (I2M, Aix-Marseille Université)
TBA
An untyped lambda-calculus generalizing Call-By-Name and Call-By-Value
Giulio Guerrieri (I2M, Aix-Marseille Université)
We introduce and study the Bang Calculus, an untyped functional calculus in which the promotion operation of Linear Logic is made explicit and where application [...]
Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system
Gilles Dowek (LSV, INRIA, ENS Paris-Saclay)
Defining a theory, such as arithmetic, geometry, or set theory, in predicate logic just requires to chose function and predicate symbols and axioms, that express [...]
21
Avr
β-réduction et développement de Taylor
Lionel Vaux (I2M, Aix-Marseille Université)
Ehrhard et Regnier ont montré au milieu des années 2000 que le développement de Taylor d’un λ-terme pur est toujours normalisable, et que sa forme [...]
31
Mar
β-réduction et développement de Taylor
Lionel Vaux (I2M, Aix-Marseille Université)
Ehrhard et Regnier ont montré au milieu des années 2000 que le développement de Taylor d’un λ-terme pur est toujours normalisable, et que sa forme [...]
From hard work to trickery: a systematic approach of probabilistic rewriting
Flavien Breuvart (PPS, Université Paris-Diderot)
Slides : https://lipn.univ-paris13.fr/~breuvart/presentations/Crecogi16.pdf http://www.pps.univ-paris-diderot.fr/~breuvart/
