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
25
Jun
02
Jul
Événements passés
20
Apr
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, [...]
Développement de Taylor extensionnel des λ-termes purs
Lionel Vaux Auclair (I2M, Aix Marseille université)
Né au début des années 2000 avec les travaux d’Ehrhard et Regnier sur le λ-calcul différentiel, le développement de Taylor des programmes et des preuves [...]
Toposes for monoid actions for complexity theory
Morgan Rogers (LIPN, Université Sorbonne Paris Nord)
This talk has three parts. First, I want to explain how common models of computation can be presented as monoid acts, which motivates the perspective [...]
An interpretation (by parametricity) of E-HA^ω inside HA^ω
Félix Castro (IRIF, Paris Cité)
HA^ω (Higher Type Arithmetic) is a first order many sorted theory. It is a conservative extension of HA (Heyting Arithmetic a.k.a the intuitionistic version of Peano Arithmetic) obtained by extending the syntax of terms to [...]
A linear monadic second-order logic over omega-words
Colin Riba (LIP, ÉNS Lyon)
(j.w.w. P. Pradic) We present LMSO, a linear logic-based variant of MSO over omega-words. LMSO can be seen as a logical syntax for a Curry-Howard-Lambek-like [...]
The theory of call-by-value solvability
Giulio Guerrieri (LIS, Aix-Marseille Université)
The semantics of the untyped (call-by-name) lambda-calculus is a well developed field built around the concept of solvable terms, which are elegantly characterized in many [...]
