Sites Inria

English version


Séminaire des équipes Gallium

Séminaire Gallium 

Inria - Paris 
2 rue Simone Iff 75012 Paris
Salle Lions 1, bâtiment C
15 octobre, 10h30

  • Date : 15/10/2018
  • Lieu : Salle Lions 1, bât C
  • Intervenant(s) : Kenji Maillard
  • Organisateur(s) : Gallium

An introduction to polarised L calculi

L calculi  , so-named after Gentzen's LK and LJ, have evolved from Curien-Herbelin's λμ̃μ by further integrating the contributions from proof theory such as focalisation and polarisation (Andreoli, Girard, …). These calculi restrict the reduction rules according to a type- or polarity-based evaluation order. Like Call-By-Push-Value, polarized calculi are an interesting vehicle to study side-effects, since they can encode and mix both call by name and call by value. However L caluli reveal the importance of linearity and thunkability, two generalizations of the idea of purity, when dealing with side-effects.

This presentation stems from an effort to write an accesible tutorial to these notions. After recalling the syntax and semantics of μ̃μ, we will explain how we introduce polarization in this setting. L calculi also admit extensions with side-effects in a rather uniform fashion and we will use this possibility to illustrate properly the notions of linearity and thunkability.

Mots-clés : Séminaire Gallium Séminaire Gallium Calcul

Haut de page

Suivez Inria