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
18
Déc
Événements passés
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/
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 [...]
