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
15
Juin
06
Juin
Journées LHC et Métayer à Paris
(...)
Voir : https://smimram.gitlabpages.inria.fr/lhc/journees/2023/04/01/journees.html
01
Juin
Profinite lambda-terms and parametricity
Vincent Moreau (IRIF)
This talk will present a definition of profinite lambda-terms of any simple type. Profinite structures naturally appear in automata theory as a way to speak [...]
25
Mai
Caractérisation de H* par le développement de Taylor extensionnel
Lionel Vaux-Auclair (I2M)
Le développement de Taylor extensionnel déjà présenté au séminaire le 9 février dernier valide les règles β et η : deux termes βη-convertibles ont des développements [...]
11
Mai
04
Mai
Quantitative inhabitation for different lambda calculi in a unifying framework
Victor Arrial (IRIF)
We study the inhabitation problem for a language called 𝜆!, a subsuming paradigm (inspired by call-by-push-value) being able to encode Call-by-Name and Call-by-Value strategies of [...]
20
Avr
Exponential functions and exponential connectives: turning the Taylor expansion into a monad
Marie Kerjean (LIPN)
TBA.
Generalized algebraic theories and categories with families
Peter Dybjer (Chalmers University of Technology, Göteborg)
We give a new syntax independent definition of the notion of a generalized algebraic theory as an initial object in a category of categories with [...]
La réduction des termes à ressources induit une extension conservative de la β-réduction sur les λ-termes
Rémy Cerda (I2M, Aix-Marseille)
Tout est dans le titre, qu’on aura peut-être le temps de prolonger par : « On a en outre des raisons raisonnables de penser que, [...]
